proposition: Lemma square_eq_pos : forall x a : R, [0] [<] a -> [0] [<] x -> x[^]2 [=] a[^]2 -> x [=] a.
proof: Proof. intros. elim (square_eq _ x a); intros; auto. exfalso. apply less_irreflexive_unfolded with (x := ZeroR). apply less_leEq_trans with x. auto. apply less_leEq. astepl ([--]a); apply inv_cancel_less. astepl ZeroR; astepr a; auto. apply Greater_imp_ap; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)