proposition: Theorem groupExp_mult : forall n2 n1 x, ((x^n1)^n2) = (x^(n1 * n2)).
proof: Proof. induction n2; intuition; simpl in *. rewrite Nat.mul_0_r. trivial. rewrite Nat.mul_comm. simpl. rewrite groupExp_plus. f_equal. rewrite IHn2. rewrite Nat.mul_comm. trivial. Qed.
imports: FCF.Rat FCF.StdNat