proposition: Lemma div2_ge_double : forall n, n >= (Nat.div2 n) + (Nat.div2 n).
proof: Proof. intuition. destruct (Nat.Even_Odd_dec n). rewrite (Nat.Even_double n) at 1. unfold Nat.double. lia. trivial. rewrite (Nat.Odd_double n) at 1. unfold Nat.double. lia. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat