proposition: Lemma prl_ne1_res1: ~ prl_ne1_some_nonempty -> forall i, inc i (psI S) -> surjection (prl_can_fun S i).
proof: Proof. rewrite /prl_ne1_some_nonempty=> H i iI. move:(prl_can_fun_fp iI) => [ff sf tf]; split => //; rewrite sf tf => y yI. case: H; ex_tac; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)