proposition: Lemma div2_compat_lt_l: forall a b, b < 2 * a -> Nat.div2 b < a.
proof: Proof. induction a; intros. - lia. - destruct b. + simpl. lia. + destruct b. * simpl. lia. * simpl. apply Nat.lt_succ_r. apply IHa. 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