proposition: Theorem groupExp_plus : forall n1 n2 x, x^(n1 + n2) = (x^n1) * (x^n2).
proof: Proof. induction n1; intuition; simpl in *. rewrite left_identity. trivial. rewrite IHn1. rewrite associativity. trivial. Qed.
imports: FCF.Rat FCF.StdNat