proposition: Theorem groupExp_distrib : forall n x y, (x * y)^n = x^n * y^n.
proof: Proof. induction n; intuition; simpl in *. rewrite left_identity. trivial. rewrite IHn. repeat rewrite associativity. f_equal. rewrite commutativity. repeat rewrite associativity. f_equal. apply commutativity. Qed.
imports: FCF.Rat FCF.StdNat