proposition: Lemma setIt_S (I:Set) (f g:I->Set): (forall i, sub (f i) (g i)) -> sub (intersectiont f) (intersectiont g).
proof: Proof. move=> su. case: (emptyset_dichot I) => i2; first by rewrite !setIt_0. move=> t /(setIt_P _ i2) hyp; apply/setIt_P => //j; apply: su;apply: hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)