proposition: Lemma greatest_partition_is_greatest x y: partition_s y x -> gle (coarser x) y (greatest_partition x).
proof: Proof. move=> pa; move: (pa) => [[pb _] _]; apply /coarser_gleP. split => //; first by apply: greatest_is_partition. move=> u /funI_P [b bx ->]. by move: bx; rewrite -pb;move /setU_P=> [z bz zy];ex_tac; move=> t /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)