proposition: Theorem modNatAddInverse_mult : forall a b c, modNat (modNatAddInverse (a * b) c) c = modNat (a * modNatAddInverse b c) c.
proof: Proof. intuition. unfold modNatAddInverse. rewrite Nat.mul_sub_distr_l. rewrite modNat_mult_eq. remember (modNat b c) as z. eapply (modNat_add_same_r (modNat (a * z) c)). rewrite Nat.sub_add. rewrite modNat_arg_eq. rewrite Nat.add_comm. rewrite <- modNat_plus. rewrite Nat.add_comm. rewrite Nat.sub_add. symmetry. apply modNat_mult. eapply Nat.mul_le_mono; intuition. subst. eapply Nat.lt_le_incl. apply modNat_lt. eapply Nat.lt_le_incl. apply modNat_lt. Qed.
imports: FCF GroupTheory OTP RndNat RndGrpElem