proposition: Lemma pos_square : forall x : R, x [#] [0] -> [0] [<] x[^]2.
proof: Proof. intros x H. elim (ap_imp_less _ _ _ H); intro H1. rstepr ([--]x[*][--]x). cut ([0] [<] [--]x). intro. apply mult_resp_pos; auto. astepl ([--]ZeroR). apply inv_resp_less. auto. rstepr (x[*]x). apply mult_resp_pos; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)