proposition: Lemma div2_even_plus : forall n m, Even n -> div2 n + m = div2 (n + (double m)).
proof: Proof. intros n m [p Hp]; apply double_inj. subst. rewrite <- !double_twice. replace (double p + double m) with (double (p + m)). now rewrite !div2_double_is_id. rewrite !double_twice; lia. Qed.
imports: Coq(Arith Lia )