proposition: Lemma prl_ne2_sigma_ne: nonempty prl_ne2_sigma.
proof: Proof. exists (psE S); apply/Zo_P; split. apply/setXb_P; split; [ exact: (ps_fgraph_E) | rewrite ps_domain_E // | ]. by rewrite FS_domain => i iI; apply: FS_whole. split => // i j lij; move: (ps_function_f lij); aw; move => [qa qb <-]. apply: (fun_image_Starget1 qa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)