proposition: Lemma sqr_nonneg : forall x : R, [0] [<=] x[^]2.
proof: Proof. intros. rewrite -> leEq_def in |- *. intro H. cut ([0] [<] x[^]2). intro H0. elim (less_antisymmetric_unfolded _ _ _ H H0). cut (x [<] [0] or [0] [<] x). intro H0. elim H0; clear H0; intros H0. rstepr ([--]x[*][--]x). cut ([0] [<] [--]x). intro H1. apply mult_resp_pos; auto. astepl ([--]([0]:R)). apply inv_resp_less. auto. rstepr (x[*]x). apply mult_resp_pos; auto. apply ap_imp_less. apply cring_mult_ap_zero with x. astepl (x[^]2). apply less_imp_ap. auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)