proposition: Lemma eqm_minus_0 : forall a b m, a ≡ b [m] <-> a - b ≡ 0 [m].
proof: Proof. intros a b m; split; intros E. rewrite E; red; f_equal; ring. rewrite <- (Zminus_0_r a), <- E; red; f_equal; ring. Qed.
imports: ZArith Znumtheory MyNat Ztools