proposition: Lemma EPfun_aux_pr2 n: natp n -> EPpermi_prop (restriction1 EPfun_aux n) n.
proof: Proof. pose H k := (restriction1 EPfun_aux k). move:(EPfun_aux_pr1) => [q1 q2 q3 q4 q5]. have fh := proj1 q1. have H0: forall k, natp k -> sub k (source EPfun_aux). by move => k kN;rewrite q2; apply: NS_inc_nat. have sjn: forall k, natp k -> surjection (H k). move => k kN;apply: (restriction1_fs fh (H0 _ kN)). have ssn: forall k, natp k -> source (H k) = k. by move => k kN; rewrite /H/ restriction1; aw. move: n; apply: Nat_induction. rewrite -/(H \0c); split => //. + exact: (proj1(sjn _ NS0)). + exact: (ssn _ NS0). + rewrite /H / restriction1; aw => t. have ww: sub \0c (source EPfun_aux) by fprops. by move/(Vf_image_P (proj1 q1) ww) => [u /in_set0]. + by move => i j /clt0. move => n nN Hrec. have snN := NS_succ nN. move: (EPpermi_next_pr1 nN Hrec). rewrite -/(H n) -/(H (csucc n)). set ph1 := extension _ _ _; move => [p1 p2 p3]. have -> // : (H (csucc n)) = ph1. have nnI: ~inc n (source (H n)). by rewrite /H/ restriction1; aw;move /(NltP nN) => []. have shn := sjn n nN. have fhn:= proj1 shn. move: (H0 _ nN)(H0 _ snN) => qa qb. apply: function_exten4 => //. + by rewrite /ph1 /extension corresp_s ! ssn // (succ_of_nat nN). + exact:(sjn _ snN). + apply: extension_fs=> //;fct_tac. + move => x; rewrite (ssn _ snN) => xi. rewrite /H restriction1_V //. move: xi;rewrite (succ_of_nat nN) => /setU1_P; case => xn. have xs: inc x (source (H n)) by rewrite (ssn _ nN). rewrite /ph1 extension_Vf_in // /H restriction1_V //. by rewrite /ph1 xn extension_Vf_out // (q5 _ nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)