proposition: Lemma setI_covering2_P x y z: inc z (intersection_covering2 x y) <-> exists a b, [/\ inc a x, inc b y & a \cap b = z].
proof: Proof. rewrite /intersection_covering2 /intersection_covering 2! identity_d. split. move/Lg_range_P => [b /setX_P [pb Pb Qb] ->]. by rewrite identity_ev // identity_ev //; exists (P b), (Q b). move => [a [b [ax iby <-]]]; apply/Lg_range_P. exists (J a b); [ fprops | aw;rewrite identity_ev // identity_ev //]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)