proposition: Lemma Exercise1_18c E: greatest_partition E = the_greatest (coarser E).
proof: Proof. move: (coarser_osr E) => [pa pb]. symmetry; apply: the_greatest_pr2 => //. have p1: partition_s (greatest_partition E) E by apply: greatest_is_partition. red; rewrite pb; split; first by apply /partitionsP. move=> x => /partitionsP xE. apply /coarser_gleP;split => // y. move /funI_P => [w wE ->]. rewrite -(proj1 (proj1 xE)) in wE; move:(setU_hi wE) => [z wz zx]. by ex_tac; move=> t /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)