proposition: Lemma mult_AbsSmall : forall x y X Y : R, AbsSmall X x -> AbsSmall Y y -> AbsSmall (X[*]Y) (x[*]y).
proof: Proof. unfold AbsSmall in |- *. intros. elim H. intros. elim H0. intros. cut ([0] [<=] X). intro. cut ([0] [<=] Y). intro. split. apply mult_AbsSmall_lft; auto. apply mult_AbsSmall_rht; auto. apply AbsSmall_nonneg with y; auto. apply AbsSmall_nonneg with x; auto. Qed.
imports: CoRN.algebra.COrdFields2