proposition: Lemma greatest_is_partition x: partition_s (greatest_partition x) x.
proof: Proof. split; last by move=> a /greatest_partition_P [w wx ->]; apply: set1_ne. split. set_extens t. move /setU_P => [y yt /greatest_partition_P [w wx swy]]. by move: yt; rewrite swy; move/set1_P => ->. move=> tx; apply/setU_P;exists (singleton t); fprops. apply /greatest_partition_P; ex_tac. move=> a b/greatest_partition_P [w wx] -> /greatest_partition_P [w' wx'] ->. mdi_tac ww => u /set1_P -> /set1_P sw; case: ww; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)