proposition: Lemma expRat_eqRat_compat : forall n r1 r2, r1 == r2 -> expRat r1 n == expRat r2 n.
proof: Proof. induction n; intuition; simpl in *; intuition. eapply ratMult_eqRat_compat; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms