proposition: Lemma div2_ge : forall n n', n >= n' -> forall x, (n' = 2 * x)%nat -> Nat.div2 n >= x.
proof: Proof. induction 1; intuition; subst; simpl in *. specialize (Nat.div2_double x); intuition; simpl in *. rewrite H. lia. destruct m. lia. destruct (Nat.Even_Odd_dec m). rewrite Nat.Even_div2. assert (Nat.div2 (S m) >= x). eapply IHle. trivial. lia. trivial. rewrite Nat.Odd_div2. eapply IHle. trivial. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat