proposition: Lemma mult_absCC : forall (x y : CC) (X Y : IR), AbsCC x [<=] X -> AbsCC y [<=] Y -> AbsCC (x[*]y) [<=] X[*]Y.
proof: Proof. intros. astepl (AbsCC x[*]AbsCC y). apply mult_resp_leEq_both. apply AbsCC_nonneg. apply AbsCC_nonneg. auto. auto. Qed.
imports: CoRN.fta.CC_Props