proposition: Lemma nexp_resp_less : forall (x y : R) n, 1 <= n -> [0] [<=] x -> x [<] y -> x[^]n [<] y[^]n.
proof: Proof. intros. induction n as [| n Hrecn]. exfalso. inversion H. elim n. simpl in |- *. astepl x. astepr y. assumption. intros. change (x[^]S n0[*]x [<] y[^]S n0[*]y) in |- *. apply mult_resp_less_both. apply nexp_resp_nonneg. assumption. assumption. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)