proposition: Lemma setIt_0 (I:Set) (f:I-> Set): I = emptyset -> intersectiont f = emptyset.
proof: Proof. move=> ie; apply /set0_P => t /Zo_S /setUt_P [i ii]. by move:(R_inc i); rewrite {2} ie => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)