proposition: Lemma AbsSmall_mult : forall e1 e2 x1 x2 : R, AbsSmall e1 x1 -> AbsSmall e2 x2 -> AbsSmall (Three[*] (e1[*]e2)) (x1[*]x2).
proof: Proof. unfold AbsSmall in |- *. intros. elim H. intros. elim H0. intros. cut ([0] [<=] e1). intro. cut ([0] [<=] e2). intro. split. apply plus_cancel_leEq_rht with (z := Three[*] (e1[*]e2)). rstepl ZeroR. rstepr (x1[*]x2[+]e1[*]e2[+]e1[*]e2[+]e1[*]e2). apply leEq_transitive with (y := x1[*]x2[+]e1[*]e2[+]x1[*]e2[+]e1[*]x2). rstepr ((e1[+]x1)[*](e2[+]x2)). apply mult_resp_nonneg. apply plus_cancel_leEq_rht with (z := [--]x1). rstepl ([--]x1). rstepr ([--][--]e1). apply inv_resp_leEq. assumption. apply plus_cancel_leEq_rht with (z := [--]x2). rstepl ([--]x2). rstepr ([--][--]e2). apply inv_resp_leEq. assumption. rstepl (x1[*]x2[+]e1[*]e2[+](x1[*]e2[+]e1[*]x2)). rstepr (x1[*]x2[+]e1[*]e2[+](e1[*]e2[+]e1[*]e2)). apply plus_resp_leEq_lft. apply plus_resp_leEq_both. apply mult_resp_leEq_rht. assumption. assumption. apply mult_resp_leEq_lft. assumption. assumption. apply plus_cancel_leEq_rht with (z := [--](x1[*]x2)). rstepl ZeroR. rstepr ([--](x1[*]x2)[+]e1[*]e2[+](e1[*]e2[+]e1[*]e2)). apply leEq_transitive with (y := [--](x1[*]x2)[+]e1[*]e2[+](x1[*]e2[-]e1[*]x2)). rstepr ((e1[+]x1)[*](e2[-]x2)). apply mult_resp_nonneg. apply plus_cancel_leEq_rht with (z := [--]x1). rstepl ([--]x1). rstepr ([--][--]e1). apply inv_resp_leEq. assumption. apply plus_cancel_leEq_rht with (z := x2). rstepl x2. rstepr e2. assumption. apply plus_resp_leEq_lft. rstepl (x1[*]e2[+][--]e1[*]x2). apply plus_resp_leEq_both. apply mult_resp_leEq_rht. assumption. assumption. rstepl (e1[*][--]x2). apply mult_resp_leEq_lft. rstepr ([--][--]e2). apply inv_resp_leEq. assumption. assumption. apply AbsSmall_nonneg with (e := e2) (x := x2). assumption. apply AbsSmall_nonneg with (e := e1) (x := x1). assumption. Qed.
imports: CoRN.algebra.COrdFields2