How to deal with division in COQ?

How to deal with with the division in a goal? Because I have a goal which is clearly true... However I cannot use lia and I think that this is related to the division.

2 ^ k / 2 ≤ 2 ^ k

Bellow is my COQ screen:

Solution

There is no automation for division on naturals - they don't even form a field. But the corresponding lemmas are not hard to find with Search:

Require Import Lia.

Goal forall k:N, 2 ^ k / 2 <= 2 ^ k.
Proof.
  intros k.
  Search (?a/?b <= ?a/?c).
  Search (_/1).
  rewrite <- N.div_1_r.
  apply N.div_le_compat_l.
  lia.
Qed.

If you have really complicated terms, you can embed the goal into reals using floor (a/b) for integer a/b and then use coq-interval. The embedding is easy to automate and coq-interval is quite powerful for proving real inequalities, but it might choke if you have more than a few floors. You can combine it with coq-gappa then to get rid of the floors. It gets quite involved then, but still fully automated. But be aware that it might not be able to prove very tight inequalities, since it uses real analysis.

Nia (Require Import Psatz), as suggested by Ana, can't solve this (and I honestly stopped trying it).