proposition: Lemma mult_AbsSmall_rht : forall x y X Y : R, [0] [<=] X -> [0] [<=] Y -> [--]X [<=] x -> x [<=] X -> [--]Y [<=] y -> y [<=] Y -> x[*]y [<=] X[*]Y.
proof: Proof. intros. rewrite -> leEq_def. intro. cut ([0] [<] x[*]y); intros. 2: apply leEq_less_trans with (X[*]Y); auto. rewrite -> leEq_def in *. cut (x[*]y [#] [0]); intros. 2: apply pos_ap_zero; auto. cut (x [#] [0]); intros. 2: apply mult_cancel_ap_zero_lft with y; auto. elim (ap_imp_less _ _ _ X3); intro. cut (y [<] [0]); intros. 2: astepl ([--][--]y); astepr ([--]([0]:R)); apply inv_resp_less. 2: apply mult_cancel_pos_rht with ([--]x). 2: astepr (x[*]y); auto. 2: astepl ([--]([0]:R)); apply less_leEq; apply inv_resp_less; auto. apply (less_irreflexive_unfolded R [1]). apply leEq_less_trans with (X[*]Y[/] _[//]X2). rstepr ((X[/] [--]x[//]inv_resp_ap_zero _ _ X3)[*] (Y[/] [--]y[//]inv_resp_ap_zero _ _ (less_imp_ap _ _ _ X4))). astepl ([1][*]([1]:R)). apply mult_resp_leEq_both. apply less_leEq; apply pos_one. apply less_leEq; apply pos_one. apply shift_leEq_div. astepl ([--]([0]:R)); apply inv_resp_less; auto. astepl ([--]x); astepr ([--][--]X); apply inv_resp_leEq; firstorder using leEq_def. apply shift_leEq_div. astepl ([--]([0]:R)); apply inv_resp_less; auto. astepl ([--]y); astepr ([--][--]Y); apply inv_resp_leEq; firstorder using leEq_def. apply shift_div_less; auto. astepr (x[*]y); auto. cut ([0] [<] y); intros. 2: apply mult_cancel_pos_rht with x; try apply less_leEq; auto. apply (less_irreflexive_unfolded R [1]). apply leEq_less_trans with (X[*]Y[/] _[//]X2). rstepr ((X[/] x[//]X3)[*](Y[/] y[//]pos_ap_zero _ _ X4)). astepl ([1][*]([1]:R)). apply mult_resp_leEq_both. apply less_leEq; apply pos_one. apply less_leEq; apply pos_one. apply shift_leEq_div; auto. astepl x; firstorder using leEq_def. apply shift_leEq_div; auto. astepl y; firstorder using leEq_def. apply shift_div_less; auto. astepr (x[*]y); firstorder using leEq_def. Qed.
imports: CoRN.algebra.COrdFields2