proposition: Lemma perm_cfun c t : perm_eq (cfun c t) t.
proof: Proof. apply/tuple_permP. pose cfunS c t := [fun i => if (i : 'I_m) <= clink c i then if (tnth t i <= tnth t (clink c i))%O then if cflip c i then (clink c i) else i else if cflip c i then i else (clink c i) else if (tnth t (clink c i) <= tnth t i)%O then if cflip c i then (clink c i) else i else if cflip c i then i else (clink c i)]. have cI : involutive (cfunS c t). move=> i /=. have cIE x : clink c (clink c x) = x by have /forallP/(_ x)/eqP := cfinv c. have cfIE x : cflip c (clink c x) = cflip c x. by have /forallP/(_ x)/eqP := cflipinv c. case: (leqP i) => [iLc|cLi]. case: (leP (tnth t i)) => [tiLtc|tcLti]. case: (boolP (cflip c i)) => [|/negPf->]; last by rewrite iLc tiLtc. rewrite !cfIE cIE => ->. case: ltngtP iLc => // [|/eqP/val_eqP <-]; first by rewrite tiLtc. by rewrite if_same. case: (boolP (cflip c i)) => [->|]; first by rewrite iLc leNgt tcLti. rewrite cfIE cIE => /negPf-> /=. rewrite (ltW tcLti); case: leqP => [|cLi]. by case: ltngtP iLc => // *; apply/val_eqP/eqP. by rewrite leNgt tcLti. case: (leP _ (tnth t i)) => [tcLti|tiLtc]. case: (boolP (cflip c i)) => [|/negPf->]. rewrite cfIE cIE => ->. by rewrite (ltnW cLi) tcLti. by rewrite leqNgt cLi tcLti. case: (boolP (cflip c i)) => [->|]. by rewrite leqNgt cLi /= leNgt tiLtc. rewrite cIE cfIE => /negPf-> /=. by rewrite (ltnW cLi) /= leNgt tiLtc. exists (perm (inv_inj cI)). apply/eqP/val_eqP; apply: eq_from_tnth => i. rewrite !tnth_map tnth_ord_tuple /= permE /=. by case: leqP => iLc; case: (cflip c i); case: leP. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple