proposition: Lemma setI_coarser_cl f g x: covering f x -> covering g x -> coarser_cg f (intersection_covering f g).
proof: Proof. move=> [fgf c1] [fgg c2]. rewrite /intersection_covering; hnf; split; aww. move => j ji; move /setX_P:(ji)=> [pj Pj Qj]; ex_tac => t. rewrite LgV //; apply: setI2_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)