proposition: Lemma setI_coarser2_clr h x: covering_s h x -> {when covering_s ^~ x &, {compat intersection_covering2 : f & / coarser_cs f h}}.
proof: Proof. move=> c23 f g c1 c2 cc1 cc2 t th. move: (cc1 _ th) (cc2 _ th)=> [b bf tb] [b' bg tb']. exists (b \cap b'). by apply/setI_covering2_P; exists b, b'. by apply: setI2_12S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)