proposition: Theorem modNat_mult_same_r : forall a b c d, modNat a d = modNat b d -> modNat (a * c) d = modNat (b * c) d.
proof: Proof. intuition. rewrite Nat.mul_comm. rewrite modNat_mult_eq. rewrite H0. rewrite <- modNat_mult_eq. rewrite Nat.mul_comm. intuition. Qed.
imports: FCF GroupTheory OTP RndNat RndGrpElem