proposition: Lemma exercise4_8c (x:= C4) (r:= (Lg C3 (fun i=> Yo (i = C0) (singleton C0) (Yo (i = C2) (singleton C1) (doubleton C2 C3))))) (s:= variantL C0 C1 (doubleton C0 C2) (doubleton C1 C3)): [/\ partition_w_fam s x, partition_w_fam r x, (forall k, inc k (domain s) -> exists2 i, inc i (domain r) & sub (Vg r i) (Vg s k)) & ~(coarser_cg s r)].
proof: Proof. move:C2_ne_C01 => [n1 n2]. move:C3_ne_C012 => [n3 n4 n5]. have nba: C1 <> C0 by fprops. have sab: (disjoint (Vg s C0) (Vg s C1)). rewrite /s; aw; apply: disjoint_pr=>u ud1 ud2. case /set2_P: ud1=> h; case /set2_P: ud2; rewrite h; auto. have ra: inc C0 C3 by apply /C3_P; in_TP4. have rb: inc C1 C3 by apply /C3_P; in_TP4. have rc: inc C2 C3 by apply /C3_P; in_TP4. have dab: disjoint (Vg r C0) (Vg r C1). rewrite !LgV//; Ytac0; Ytac0; Ytac0; Ytac0. apply: disjoint_pr=> u /set1_P -> /set2_P; case; auto. have dac: disjoint (Vg r C0) (Vg r C2). rewrite !LgV//; Ytac0; Ytac0; Ytac0; Ytac0. apply: disjoint_pr=> u /set1_P -> /set1_P; auto. have dcb: disjoint (Vg r C2) (Vg r C1). rewrite !LgV//; Ytac0; Ytac0; Ytac0; Ytac0. apply: disjoint_pr=> u /set1_P -> /set2_P; case; auto. split. rewrite /s;split; fprops. rewrite /variantL;red; aw; move=> i j ids jds. case /set2_P: ids => ->; case /set2_P: jds =>->; auto. by right; apply:disjoint_S. set_extens y => ys. case (setUb_hi ys); aw; move=> z zd. case /set2_P: zd => ->; aw=> yd; case /set2_P: yd => ->; apply/C4_P;in_TP4. case /C4_P: ys; move => ->. by apply :(@setUb_i _ C0);aw; fprops. by apply :(@setUb_i _ C1);aw; fprops. by apply :(@setUb_i _ C0);aw; fprops. by apply :(@setUb_i _ C1);aw; fprops. split; first by rewrite /r; fprops. red; rewrite {1 2} /r; aw; move=> i j idr jdr. case /C3_P:idr => ->;case /C3_P:jdr;try move => ->; auto; try case => ->; auto; by right;apply: disjoint_S. set_extens t => ts. move: (setUb_hi ts); rewrite /r;aw; move => [y ydr]; rewrite LgV//. case /C3_P:ydr => ->; Ytac0; Ytac0; try move /set1_P ->; try case/set2_P => ->; apply /C4_P;in_TP4. rewrite /r; case /C4_P: ts; [set v := C0 | set v := C2 | set v := C1 | set v := C1 ]; move => ->; apply: (@setUb_i _ v); aw; trivial; rewrite LgV//; Ytac0; Ytac0; fprops. rewrite /s/r; aw; move => k kds; case /set2_P: kds =>->. exists C0 => //; aw;rewrite LgV//; Ytac0; Ytac0 => t /set1_P ->; fprops. exists C2 => //; aw; rewrite LgV//; Ytac0; Ytac0 => t /set1_P ->; fprops. move=> [_ _ ]; rewrite {1}/r;aw => cc. move: (cc _ rb) => [i]; rewrite /s; aw=> ids. rewrite LgV//; Ytac0; Ytac0. case /set2_P: ids=> ->; aw => h. move: (h _ (set2_2 C2 C3)) => /set2_P; case; auto. move: (h _ (set2_1 C2 C3)) => /set2_P; case; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)