proposition: Lemma setXb_monotone1 f g: domain f = domain g -> (forall i, inc i (domain f) -> sub (Vg f i) (Vg g i)) -> sub (productb f) (productb g).
proof: Proof. move=> dfdg sVV x /setXb_P [fx dx iVV]. apply/setXb_P; rewrite -dfdg;split => // i ifg; apply: sVV; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)