proposition: Lemma setI_P y: nonempty y -> forall x, (inc x (intersection y) <-> (forall i, inc i y -> inc x i)).
proof: Proof. by move=> ney; split; [ move=> xi iy; apply: setI_hi | apply: setI_i]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)