proposition: Lemma setI_coarser2_cl f g x: covering_s f x -> covering_s g x -> coarser_cs f (intersection_covering2 f g).
proof: Proof. move=> c1 c2 z; move/setI_covering2_P=> [a [b [af bg <-]]]. ex_tac; apply: subsetI2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)