proposition: Lemma expRat_le_1 : forall n x, x <= 1 -> expRat x n <= 1.
proof: Proof. induction n; intuition; simpl in *. intuition. eapply leRat_trans. eapply ratMult_leRat_compat. eapply H. eapply IHn. trivial. rewrite ratMult_1_l. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms