proposition: Lemma EPperm_compat0_exists r n h x: natp n -> n <> \0c -> total_order r -> (inc x (substrate r)) -> (forall i, i <c n -> inc (h i) (substrate r)) -> (forall i, i <c n -> (h i) <> x) -> exists k, (EPperm_compat0 r h n k x).
proof: Proof. move => nN nz [or tor] xsr hsr xnr. move:(cpred_pr nN nz) => [sa sb]. have nn:= (cpred_lt nN nz). have cpi: inc (cpred n) n by apply /(NltP nN). set y := h (cpred n). have ysr: inc y (substrate r) by apply: hsr. have xny: y <> x by apply: xnr. case: (tor _ _ ysr xsr) => lta. exists n; split; fprops. + by move => ha;case: (@succ_nz (cpred n)). + by move => _ _. + by case. pose prop z := z <c n /\ glt r x (h z). have nE: prop (cpred n) by split => //;split => //; apply: nesym. case:(least_int_prop2 sa nE). by move => [/proj1 qa [qb qc]]; exists \0c; split. set i := cpred _; move => [iN [ha hb]] aE. have lin:=(cle_ltT (cleS iN) ha). have hc:inc i n by apply/(NltP nN). have hix: h i <> x by apply:xnr. have he: glt r (h i) x. case: (tor _ _ (hsr _ lin) xsr) => // hf. by case: aE; split => //; split => //; apply: nesym. exists (csucc i); split. + exact: (proj1 ha). + by move => hw; case: (@succ_nz i). + by move: (proj2 ha). + by move => ua ub; rewrite (cpred_pr2 iN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)