proposition: Lemma expRat_base_prod : forall n r1 r2, expRat (r1 * r2) n == (expRat r1 n) * (expRat r2 n).
proof: Proof. induction n; intuition; simpl in *. symmetry. eapply ratMult_1_l. rewrite IHn. repeat rewrite <- ratMult_assoc. eapply ratMult_eqRat_compat; intuition. repeat rewrite ratMult_assoc. eapply ratMult_eqRat_compat; intuition. eapply ratMult_comm. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms