proposition: Lemma mult_AbsSmall'_rht : forall x y C : R, [0] [<=] C -> [--]C [<=] x -> x [<=] C -> [--]C [<=] y -> y [<=] C -> x[*]y [<=] Three[*]C[^]2.
proof: Proof. intros. astepl ([0][+]x[*]y). apply shift_plus_leEq. apply leEq_transitive with ((C[+]x)[*](C[-]y)). apply mult_resp_nonneg. apply shift_leEq_plus. astepl ([--]x). astepr ([--][--]C). apply inv_resp_leEq. auto. apply shift_leEq_minus. astepl y. auto. rstepl (C[^]2[-]x[*]y[+]C[*](x[-]y)). rstepr (C[^]2[-]x[*]y[+]C[*](C[-][--]C)). apply plus_resp_leEq_lft. apply mult_resp_leEq_lft. apply minus_resp_leEq_both. auto. auto. auto. Qed.
imports: CoRN.algebra.COrdFields2