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