proposition: Lemma nexp_resp_leEq_one : forall c : R, [0] [<=] c -> c [<=] [1] -> forall n, c[^]n [<=] [1].
proof: Proof. simple induction n. red in |- *; apply eq_imp_leEq. algebra. clear n; intros. astepl (c[^]n[*]c). astepr (([1]:R)[*][1]). apply mult_resp_leEq_both; auto. apply nexp_resp_nonneg; assumption. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)