proposition: Lemma div2_le_mono : forall n1 n2, (n1 <= n2 -> Nat.div2 n1 <= Nat.div2 n2)%nat.
proof: Proof. assert (I : 0 < 2) by now apply Nat.lt_0_succ. intros n1 n2; destruct (Nat.Even_Odd_dec n1) as [[k1 ->] | [k1 ->]]; destruct (Nat.Even_Odd_dec n2) as [[k2 ->] | [k2 ->]]; intros H. - now rewrite 2!Nat.div2_double; apply Nat.mul_le_mono_pos_l with (1 := I). - rewrite Nat.div2_double, Nat.add_1_r, Nat.div2_succ_double. apply Nat.mul_le_mono_pos_l with (1 := I). lia. - rewrite Nat.div2_double, Nat.add_1_r, Nat.div2_succ_double. apply Nat.mul_le_mono_pos_l with (1 := I). lia. - rewrite 2!Nat.add_1_r, 2!Nat.div2_succ_double. lia. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat