proposition: Lemma expRat_le' : forall n1 n2 r v, expRat r n1 <= v -> ~ (1 <= r) -> n2 >= n1 -> expRat r n2 <= v.
proof: Proof. intuition. eapply leRat_trans. eapply expRat_le. case_eq (bleRat r 1); intuition. exfalso. eapply H0. eapply bleRat_total. trivial. eauto. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms