proposition: Lemma exercise4_8b (r:= Lg (singleton C0) (fun _ => C2)) (s:= variantL C0 C1 C2 (singleton C0)) : [/\ covering r C2, covering s C2, coarser_cg s r, nonempty_fam s & ~(forall k, inc k (domain s) -> exists i, inc i (domain r) /\ sub (Vg r i) (Vg s k))].
proof: Proof. have ba := C1_ne_C0. rewrite /r/s;split. - split; fprops; move=> t tx; apply: (@setUb_i _ C0); fprops; aw; fprops. rewrite LgV; fprops. - split; fprops; move=> y yx;apply: (@setUb_i _ C0); fprops; aw; fprops. - split; fprops; aw => t /set1_P ->; exists C0; first fprops. aw; rewrite LgV;fprops. - move=> k; aw => kd ;rewrite LgV //;case /set2_P:kd=> ->; aw;apply: set2_ne. aw; move=> h; move: (h _ inc_C1_C2)=> [i [/set1_P ->]]; aw. rewrite LgV; fprops => xa. by move: (xa _ inc_C1_C2) => /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)