proposition: Lemma mult_resp_leEq_rht : forall x y z : R, x [<=] y -> [0] [<=] z -> x[*]z [<=] y[*]z.
proof: Proof. intros x y z . repeat rewrite -> leEq_def. intros H H0 H1. generalize (shift_zero_less_minus _ _ _ H1); intro H2. cut ([0] [<] (x[-]y) [*]z). intro H3. 2: rstepr (x[*]z[-]y[*]z). 2: assumption. cut (forall a b : R, [0] [<] a[*]b -> [0] [<] a and [0] [<] b or a [<] [0] and b [<] [0]). intro H4. generalize (H4 _ _ H3); intro H5. elim H5; intro H6. elim H6; intros. elim H. astepl ([0][+]y). apply shift_plus_less. assumption. elim H6; intros. elim H0. assumption. 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 H9. assumption. exfalso. elim (less_irreflexive_unfolded R [0]). apply less_leEq_trans with (a[*]b). assumption. apply less_leEq. apply inv_cancel_less. astepl ([0]:R). astepr ([--]a[*]b). apply mult_resp_pos. astepl ([--]([0]:R)). apply inv_resp_less. assumption. assumption. left. split. assumption. elim (ap_imp_less _ _ _ H7); intro H9. exfalso. elim (less_irreflexive_unfolded R [0]). apply less_leEq_trans with (a[*]b). assumption. apply less_leEq. apply inv_cancel_less. astepl ([0]:R). astepr (a[*][--]b). apply mult_resp_pos. assumption. astepl ([--]([0]:R)). apply inv_resp_less. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)