proposition: Lemma mult_pos_imp : forall a b : R, [0] [<] a[*]b -> [0] [<] a and [0] [<] b or a [<] [0] and b [<] [0].
proof: Proof. generalize I; intro. generalize I; intro. generalize I; intro. generalize I; intro. generalize I; intro. intros a b H4. generalize (Greater_imp_ap _ _ _ H4); intro H5. generalize (mult_cancel_ap_zero_lft _ _ _ H5); intro H6. generalize (mult_cancel_ap_zero_rht _ _ _ H5); intro H7. elim (ap_imp_less _ _ _ H6); intro H8. right. split. assumption. elim (ap_imp_less _ _ _ H7); intro. assumption. exfalso. elim (less_irreflexive_unfolded R [0]). apply less_leEq_trans with (a[*]b). assumption. apply less_leEq. apply inv_cancel_less. astepl ZeroR. astepr ([--]a[*]b). apply mult_resp_pos. astepl ([--]ZeroR). apply inv_resp_less. assumption. assumption. left. split. assumption. elim (ap_imp_less _ _ _ H7); intro. exfalso. elim (less_irreflexive_unfolded R [0]). apply less_leEq_trans with (a[*]b). assumption. apply less_leEq. apply inv_cancel_less. astepl ZeroR. astepr (a[*][--]b). apply mult_resp_pos. assumption. astepl ([--]ZeroR). apply inv_resp_less. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)