proposition: Lemma setI_sub2 x y: (forall i, inc i y -> sub i x) -> sub (intersection y) x.
proof: Proof. move=> hyp. case: (emptyset_dichot y) => ie; first by rewrite ie setI_0; fprops. case: ie => i iy; exact:(sub_trans (setI_s1 iy) (hyp _ iy)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)