proposition: Lemma setI_coarser_clr h x: covering h x -> {when covering ^~ x &, {compat intersection_covering : f & / coarser_cg f h}}.
proof: Proof. move => c3 f g c1 c2 [fgf fhg cc1] [fgg _ cc2]. rewrite /intersection_covering /coarser_cg; split;aww. move => u udh. move: (cc2 _ udh)(cc1 _ udh) => [i isg s1] [j jsf s2]. have pd: inc (J j i) (domain f \times domain g) by fprops. exists (J j i) => //; rewrite LgV //; aw. by move=> v vh; apply/setI2_i; [apply: s2 |apply: s1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)