proposition: Lemma setI_i x a: nonempty x -> (forall y, inc y x -> inc a y) -> inc a (intersection x).
proof: Proof. move => [y yx] all_ayx; apply: Zo_i=> //. move: (all_ayx _ yx) (yx); apply: setU_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)