proposition: Theorem cprod_increasing f g: domain f = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x)) -> (cprod f) <=c (cprod g).
proof: Proof. move=> dfdg alle. by apply: sub_smaller; apply: setXb_monotone1 =>// i /alle [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)