proposition: Lemma EPpermi_exten h1 h2 n k: natp n -> n <> \0c -> (forall i, i<c n -> h1 i = h2 i) -> EPpermi_fct h1 n k = EPpermi_fct h2 n k.
proof: Proof. move => nn nz sv. rewrite /EPpermi_fct; apply: f_equal. have zn1: \0c <c n by apply: card_ne0_pos; fprops. have cp1: cpred n <c n by apply: cpred_lt. apply:Zo_exten2 => x; rewrite /EPperm_compat0. rewrite (sv _ zn1) (sv _ cp1). case: (equal_or_not k \0c) => kz. split; move => [xN [pa pb pc pd]]; split =>//; split => //. case: (equal_or_not k n) => kn. rewrite kn;split; move => [xN [pa pb pc pd]]; split =>//; split => // [][] //. case (p_or_not_p ( k <=c n)) => hh; last first. split; move => [xN [pa _ _ _]]; split =>//; split => //. have ckn: cpred k <c n. move:(cpred_pr (NS_le_nat hh nn) kz) => [sa sb]. by apply /(cleSltP sa); rewrite - sb. rewrite sv // sv //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)