proposition: Lemma EPperm_compat_uniq s n i j: natp n -> EPperm_M s n -> EPperm_compat s n i -> EPperm_compat s n j -> i = j.
proof: Proof. move => pc [pd pe] [lin qa qb qc] [ljn qa' qb' qc']. have or: order r1 by move:eta_like_r1 => [[[]]]. have jN:= NS_le_nat ljn pc. have iN:= NS_le_nat lin pc. have aux1: n <> \0c -> \0c <c n by apply:card_ne0_pos; fprops. pose F i := (Vf f (Vf s i)). have rpe: forall i j, i <c n -> j <c n -> glt r1 (F i) (F j) -> i <c j. move => i1 j1 lin1 ljn1 [le1 ne1]. case: (cleT_ell (proj31_1 lin1)(proj31_1 ljn1)) => // h. by case: ne1; rewrite h. move:(pe _ _ h lin1) => le2; order_tac. have re: forall k, k <=c n -> glt r1 (F (cpred k)) (F \0c) -> False. move => k lkn H. case: (equal_or_not k \0c) => knz. by case:(proj2 H); rewrite knz cpred0. have ha:= (clt_leT (cpred_lt (NS_le_nat lkn pc) knz) lkn). case: (equal_or_not n \0c) => nz. by case knz; apply: (cle0); rewrite - nz. by move: (rpe _ _ ha (aux1 nz) H) => /(clt0). case: (equal_or_not i \0c) => iz. case: (equal_or_not j \0c) => jz; first by rewrite iz jz. have ha: glt r1 (Vf f (Vf s (cpred j))) (Vf f n). case: (equal_or_not j n) => jn; first by move:(qb' jn jz); rewrite jn. by case: (qc' (conj ljn jn) jz). case:(re _ ljn (lt_lt_trans or ha (qa iz))). case:(equal_or_not n \0c) => enz; first by case: iz; apply:cle0; ue. have Ha: glt r1 (Vf f (Vf s (cpred i))) (Vf f n). case: (equal_or_not i n) => jn; first by move:(qb jn iz); rewrite jn. by case:(qc (conj lin jn) iz). have rf: forall k, k <c n -> ~ glt r1 (Vf f (Vf s (cpred n))) (Vf f (Vf s k)). move => k kn H. have [sa sb]:=(cpred_pr pc enz). move:(rpe _ _ (cpred_lt pc enz) kn H) =>/(cleSltP sa). by rewrite - sb => /(cltNge kn). have [sa sb]:=(cpred_pr iN iz). case: (equal_or_not i n) => ein. rewrite ein in iz sa sb |- *. case: (equal_or_not j \0c) => jnz. case: (re _ lin (lt_lt_trans or Ha (qa' jnz))). ex_middle jn; move:(conj ljn (nesym jn)) => ltjn; case: (rf j ltjn). by move:(lt_lt_trans or Ha (proj2 (qc' ltjn jnz)));rewrite ein. have Hb:= (proj2 (qc (conj lin ein) iz)). have sc: (cpred i) <c n by apply/(cleSltP sa); rewrite - sb. case:(equal_or_not j \0c) => jz. case:(re _ lin (lt_lt_trans or Ha (qa' jz))). case:(equal_or_not j n) => jn. by move:(lt_lt_trans or (qb' jn jz) Hb) => ha; case: (rf i (conj lin ein)). move: (qc' (conj ljn jn) jz) => [Hc Hd]. have [sa1 sb1]:=(cpred_pr jN jz). have sd: (cpred j) <c n by apply/(cleSltP sa1); rewrite - sb1. move:(rpe _ _ sc (conj ljn jn) (lt_lt_trans or Ha Hd)) => ra. move:(rpe _ _ sd (conj lin ein) (lt_lt_trans or Hc Hb)) => rb. case: (NleT_ell iN jN); first by exact. by rewrite sb1; move/(cltSleP sa1) => /(cltNge rb). by rewrite sb; move/(cltSleP sa) => /(cltNge ra). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)