proposition: Lemma nexp_resp_great_One : forall (OF : COrdField) (x : OF), [1][<]x -> forall n : nat, [1][<=]x[^]n.
proof: Proof. intros. change (x[^]0[<=]x[^]n) in |- *. apply great_nexp_resp_le. apply less_leEq; assumption. apply Nat.le_0_l. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon