proposition: Lemma least_is_partition x: nonempty x -> partition_s (least_partition x) x.
proof: Proof. rewrite /least_partition=>ne. split; last by move=> a /set1_P ->. split; first by apply: setU_1. by move=> a b /set1_P -> /set1_P ->; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)