proposition: Lemma partition_nq_pr5 E: (partition_nq E \1c) = singleton (greatest_partition E).
proof: Proof. set p := greatest_partition E. have ha: inc p (partition_nq E \1c). apply /Zo_P; split; first apply: Zo_i. - by apply/setP_P => t /funI_P [z zE ->]; apply/setP_P => x /set1_P ->. - exact:greatest_is_partition. - by move => x /funI_P [z zE ->]; rewrite cardinal_set1. apply: (set1_pr ha) => z /Zo_P [/Zo_P [/setP_P hc [[hb _] _]] hd]. set_extens t. move => tz; apply/funI_P. move/set_of_card_oneP :(hd _ tz) => [x tx]; exists x => //. move /setP_P: (hc _ tz); apply; rewrite tx; fprops. move => /funI_P [x xE ->]. move: xE; rewrite - hb => /setU_P [y xy yz]. move/set_of_card_oneP :(hd _ yz) => [x' tx']. by rewrite tx' in xy; rewrite (set1_eq xy) - tx'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)