proposition: Lemma prl_ne1_res3 A: cofinal (psr S) A -> finite_set A -> forall i, inc i (psI S) -> surjection (prl_can_fun S i).
proof: Proof. move => [sra cfa] fa. case: (emptyset_dichot (psI S)) => neI. by rewrite neI => i /in_set0. move:(proj33 (ps_preorder_r S)) => ot. have HA: forall x, finite_set x -> (sub x (substrate (psr S)) -> exists y, upper_bound (psr S) x y). apply: finite_set_induction. move => _; move: neI => [y yI]; exists y => //; split. by rewrite ps_substrate_r. by move => t /in_set0. move => a b h1 h2; move:(h1(sub_trans (@subsetU2l _ _) h2)) => [y [ya yb]]. have bsr := (h2 _ (setU1_1 a b)). move:(rdr ya bsr) => [z [za zb]]; exists z; split => //; first by order_tac. move => t /setU1_P [ta | -> //]; by exact:(ot _ _ _ (yb _ ta) za). move: (HA _ fa sra) => [y [ya yb]]. apply:prl_ne1_res2; exists y; first by rewrite - ps_substrate_r. rewrite - ps_substrate_r. move => i iI; move:(cfa _ iI) => [z /yb za] le; apply: (ot _ _ _ le za). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)