proposition: Theorem modNat_mult_eq : forall a b c, modNat (a * b) c = modNat (a * modNat b c) c.
proof: Proof. intuition. destruct (modNat_correct b c). rewrite H. clear H; rewrite Nat.mul_add_distr_l. rewrite modNat_plus. rewrite Nat.mul_assoc. rewrite modNat_mult. rewrite Nat.add_0_l. symmetry. rewrite modNat_plus. rewrite modNat_mult. rewrite Nat.add_0_l. rewrite (@modNat_eq _ (modNat b c)). trivial. eapply modNat_lt. Qed.
imports: FCF GroupTheory