proposition: Lemma eqm_square_half : forall x m, 0 <> m -> x ≡ m [2 * m] -> x * x ≡ m * m [4 * (m * m)].
proof: Proof. intros x m Nm D. rewrite eqm_minus_0 in D. rewrite divide_eqm in D; notzero. destruct (Zdivide_inf _ _ D) as (k, Ek). replace x with (x - m + m) by ring. rewrite Ek. apply eqm_minus_0. ring_simplify. apply divide_eqm; notzero. exists (k + k ^ 2). ring. Qed.
imports: ZArith Znumtheory MyNat Ztools