proposition: Lemma expRat_exp_sum : forall n1 n2 r, expRat r (n1 + n2)%nat == (expRat r n1) * (expRat r n2).
proof: Proof. induction n1; intuition; simpl in *. symmetry. eapply ratMult_1_l. rewrite IHn1. rewrite ratMult_assoc. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms