proposition: Lemma root_unique : forall x y : R, [0] [<=] x -> [0] [<=] y -> forall n, 0 < n -> x[^]n [=] y[^]n -> x [=] y.
proof: Proof. intros. apply leEq_imp_eq. apply power_cancel_leEq with n; auto. astepr (x[^]n). apply leEq_reflexive. apply power_cancel_leEq with n; auto. astepl (x[^]n). apply leEq_reflexive. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)