proposition: Lemma root_one : forall x : R, [0] [<=] x -> forall n, 0 < n -> x[^]n [=] [1] -> x [=] [1].
proof: Proof. intros. apply root_unique with n; auto. apply less_leEq. apply pos_one. Step_final ([1]:R). Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)