proposition: Lemma div2_incr : forall n m, n <= m -> div2 n <= div2 m.
proof: Proof. intros n m; destruct (nat_double_or_s_double n) as [[p Hp] | [p Hp]]; subst; destruct (nat_double_or_s_double m) as [[q Hq] | [q Hq]]; subst. - rewrite !div2_double_is_id ;unfold double; lia. - rewrite !div2_double_is_id, !double_twice, div2_succ_double; lia. - rewrite (double_twice p), div2_succ_double; rewrite !div2_double_is_id, double_twice; lia. - rewrite !double_twice; rewrite !div2_succ_double. lia. Qed.
imports: Coq(Arith Lia )