proposition: Lemma two_times_div2_bound: forall n, 2 * Nat.div2 n <= n.
proof: Proof. eapply strong. intros n IH. destruct n. - constructor. - destruct n. + simpl. constructor. constructor. + simpl (Nat.div2 (S (S n))). specialize (IH n). lia. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Bool.Bool Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith bbv.N_Z_nat_conversions bbv.Nomega