proposition: Lemma EPfun_aux_pr1 (h := EPfun_aux) : [/\ surjection h, source h = Nat, sub (target h) Nat, Vf h \0c = \0c & forall n, natp n -> Vf h n = EPpermi_next (restriction1 h n) n].
proof: Proof. move:Nat_order_wor => [pa pb]. move:(transfinite_defined_pr (fun u => (EPpermi_next u (source u))) pa). rewrite -/EPfun_aux -/h; move => [ha hb hc]. rewrite pb in hc hb. have hh: forall x, natp x -> source (restriction1 h (segment Nat_order x)) = x. move => x xN; rewrite / restriction1; aw. by rewrite (segment_Nat_order1 xN). have sth: sub (target h) Nat. move => t /(proj2 ha) [n nN ->]; rewrite hb in nN. rewrite (hc _ nN) /EPpermi_next; Ytac w; [exact: NS0 |exact: EPpermi_pr0]. split => //. by rewrite (hc _ NS0) (hh _ NS0) / EPpermi_next; Ytac0. move => n nN. rewrite (hc _ nN) (hh _ nN) . by rewrite (segment_Nat_order1 nN) - (NintE nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)