proposition: Lemma Exercise1_18a E: complete_lattice (coarser E).
proof: Proof. move: (coarser_osr E) => [coE soE]. apply: (Exercise1_11b coE). have aux: forall u, inc u (substrate (coarser E)) <-> partition_s u E. by move=> u; rewrite soE; apply/partitionsP. move=> X XsE;case: (emptyset_dichot X) => neX; last first. set (f := identity_g X). have fgf: (fgraph f) by apply: identity_fgraph. have rf: (range f = X) by apply: identity_r. have df: (domain f = X) by apply: identity_d. rewrite -df in neX; rewrite -rf. exists (intersection_partition f);apply: (intersection_is_sup fgf _ neX). by rewrite/allf df /f => u uX; rewrite (identity_ev uX); move/aux:(XsE _ uX). rewrite neX. case: (emptyset_dichot E) => Ee. have pE: (partition_s emptyset E). split; last by move=> a /in_set0. split; [by rewrite Ee setU_0 | by move=> a b /in_set0 ]. exists emptyset; rewrite lub_set0 //; split;first by apply/ aux. move => x /aux xE; apply /coarser_gleP; split => //; move=> t tx. move:(proj2 xE _ tx) => [w wt]. move: (proj1(proj1 xE)); rewrite Ee => p1; empty_tac1 w; union_tac. exists (least_partition E). rewrite lub_set0 //; split. by apply/ aux; apply: least_is_partition. move=> x /aux px; apply/coarser_gleP; split => //. by apply: least_is_partition. move=> a ax; exists E; first by rewrite /least_partition; fprops. by rewrite - (proj1(proj1 px)); apply: setU_s1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)