proposition: Lemma mult_resp_less_both : forall x y u v : R, [0] [<=] x -> x [<] y -> [0] [<=] u -> u [<] v -> x[*]u [<] y[*]v.
proof: Proof. cut (forall x y z : R, x [<=] y -> [0] [<=] z -> x[*]z [<=] y[*]z). intro resp_leEq. intros. apply leEq_less_trans with (y[*]u). apply resp_leEq; auto. apply less_leEq; auto. apply mult_resp_less_lft; auto. apply leEq_less_trans with x; auto. intros x y z. repeat rewrite -> leEq_def in |- *. 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); auto. 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 H7 H8. apply H. astepl ([0][+]y). apply shift_plus_less. assumption. apply 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; auto. elim (ap_imp_less _ _ _ H7); auto. intro H9. exfalso. apply (less_irreflexive_unfolded R [0]). apply less_leEq_trans with (a[*]b); auto. apply less_leEq. apply inv_cancel_less. astepl ([0]:R). astepr ([--]a[*]b). apply mult_resp_pos; auto. astepl ([--]([0]:R)). apply inv_resp_less; auto. left. split; auto. elim (ap_imp_less _ _ _ H7); auto. intro H9. exfalso. apply (less_irreflexive_unfolded R [0]). apply less_leEq_trans with (a[*]b); auto. apply less_leEq. apply inv_cancel_less. astepl ([0]:R). astepr (a[*][--]b). apply mult_resp_pos; auto. astepl ([--]([0]:R)). apply inv_resp_less; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)