proposition: Lemma least_partition_is_least x y: nonempty x -> partition_s y x -> gle (coarser x) (least_partition x) y.
proof: Proof. move=> nex pa;apply/coarser_gleP;split => //; first by apply:least_is_partition. move=> u uy; rewrite /least_partition. by ex_tac; move:(partition_set_in_PP pa) => /setP_P yp; apply/setP_P; apply: yp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)