proposition: Lemma power_cancel_less : forall (x y : R) k, [0] [<=] y -> x[^]k [<] y[^]k -> x [<] y.
proof: Proof. intros x y k H H0. elim (zerop k); intro y0. rewrite y0 in H0. cut ([1] [<] ([1]:R)). intro H1. elim (less_irreflexive_unfolded _ _ H1). astepl (x[^]0). astepr (y[^]0). auto. cut (x [<] y or y [<] x). intro H1. elim H1; clear H1; intros H1. auto. cut (x [<=] y). intro. destruct (leEq_def _ x y) as [H3 _]. elim ((H3 H2) H1). apply power_cancel_leEq with k; auto. apply less_leEq. auto. apply ap_imp_less. apply un_op_strext_unfolded with (nexp_op (R:=R) k). apply less_imp_ap. auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)