proposition: Lemma great_nexp_resp_le : forall (x : R) m n, [1] [<=] x -> m <= n -> x[^]m [<=] x[^]n.
proof: Proof. intros. induction n as [| n Hrecn]; intros. replace m with 0. apply leEq_reflexive. auto with arith. elim (le_lt_eq_dec _ _ H0); intro. astepl (x[^]m[*][1]). astepr (x[^]n[*]x). apply mult_resp_leEq_both; auto with arith. apply nexp_resp_nonneg; auto. apply leEq_transitive with ([1]:R); auto. apply less_leEq. apply pos_one. apply less_leEq. apply pos_one. rewrite b. apply leEq_reflexive. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)