proposition: Lemma power_cancel_leEq : forall (x y : R) k, 0 < k -> [0] [<=] y -> x[^]k [<=] y[^]k -> x [<=] y.
proof: Proof. intros x y k H. repeat rewrite -> leEq_def. intros H0 H1 H2. apply H1. apply nexp_resp_less; try rewrite -> leEq_def; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)