proposition: Lemma square_eq_neg : forall x a : R, [0] [<] a -> x [<] [0] -> 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 leEq_less_trans with x. astepr a; apply less_leEq; auto. auto. apply Greater_imp_ap; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)