proposition: Lemma rcs_perm_ffun_injectiveb n : injectiveb (@rcs_perm_ffun n).
proof: Proof. apply/injectiveP => x y. rewrite /rcs_perm_ffun 2!ffunE. case: ifPn => [/eqP ->|x0]. case: ifPn => [/eqP -> //|y0]. move/eqP; rewrite -val_eqE /= => /eqP n0y. exfalso; move: (ltn_ord y). rewrite ltnNge => /negP; apply. rewrite [in X in X < _]n0y /= inordK //; first by rewrite prednK // lt0n. apply: ltn_trans (ltn_ord y); by rewrite prednK // lt0n. case: ifPn => [/eqP -> //|y0 /eqP]. move/eqP; rewrite -val_eqE /= => /eqP n0x. exfalso; move: (ltn_ord x). rewrite ltnNge => /negP; apply. rewrite -[in X in X < _]n0x /= inordK //; first by rewrite prednK // lt0n. apply: ltn_trans (ltn_ord x); by rewrite prednK // lt0n. rewrite -val_eqE /= inordK; last first. apply: (ltn_trans _ (ltn_ord x)); by rewrite prednK // lt0n. rewrite inordK; last first. apply: (ltn_trans _ (ltn_ord y)); by rewrite prednK // lt0n. move/eqP/(congr1 S). by rewrite prednK ?lt0n // prednK ?lt0n // => ?; apply val_inj. Defined.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly polydiv vector) ssralg_ext poly_ext f2 hamming linearcode dft