proposition: Lemma exercise4_8a r s x: covering r x -> covering s x -> partition_w_fam s x -> coarser_cg s r -> nonempty_fam s -> forall k, inc k (domain s) -> exists2 i, inc i(domain r) & sub (Vg r i) (Vg s k).
proof: Proof. move=> [fgr co1] [fgs co2] [fgL md usx] [_ _ co] alne k kds. move: (alne _ kds)=> [y ysk]. have yx: inc y x by rewrite -usx;apply: (@setUb_i _ k);aw. have yu: inc y (unionb r) by apply: co1. move: (setUf_hi yu)=> [z zdr yrz]. move: (co _ zdr)=> [i ids rsi]. have yri: inc y (Vg s i) by apply: rsi. move: md; rewrite /mutually_disjoint; aw=> aux; case: (aux _ _ kds ids). by move=> ->; ex_tac. by move=> h; empty_tac1 y;aw; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)