proposition: Lemma div2_double : forall n, div2 (2 * n) = n.
proof: Proof. induction n as [ | n IHn]. - simpl;auto. - replace (2 * S n) with (S (S (2 * n))) by lia. simpl in *; now rewrite IHn. Qed.
imports: Arith ArithRing Lia Recdef