proposition: Lemma mult_resp_nonneg : forall x y : R, [0] [<=] x -> [0] [<=] y -> [0] [<=] x[*]y.
proof: Proof. intros x y. repeat rewrite -> leEq_def. intros H H0 H1. apply H0. cut (x[*]y [#] [0]). intro H2. cut (x [#] [0]). intro H3. cut (y [#] [0]). intro H4. elim (ap_imp_less _ _ _ H4); intro H5. auto. elim (ap_imp_less _ _ _ H3); intro H6. elim (H H6). elim (less_antisymmetric_unfolded _ _ _ H1 (mult_resp_pos _ _ _ H6 H5)). apply cring_mult_ap_zero_op with x. auto. apply cring_mult_ap_zero with y. auto. apply less_imp_ap. auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)