proposition: Lemma setI_covering E: {compat intersection_covering : x & / covering x E}.
proof: Proof. move => f g [fgf c1] [fgg c2]. rewrite /intersection_covering; split; first by fprops. move => u ux; move /setUb_P: (c1 _ ux) => [a af uf]. move/setUb_P:(c2 _ ux)=> [b bg ug]. have jj: inc (J a b) (domain f \times domain g) by fprops. apply/setUb_P;aw;exists (J a b) => //; rewrite LgV //; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)