proposition: Lemma div2_double_is_id :forall n : nat, div2 (double n) = n.
proof: Proof. induction n as [ | n IHn]. - reflexivity. - replace (double (S n)) with (S (S (double n))). replace (S n) with (S (div2 (double n))); auto. symmetry. unfold double; lia. Qed.
imports: Coq(Arith Lia )