proposition: Lemma perm_ids_inj : injective perm_ids.
proof: Proof. rewrite /perm_ids => i j. move: (splitP (ord_split i)) => [i' Hi'|i' Hi']. move: (splitP (ord_split j)) => [j' Hj'|j' Hj']. move/eqP. rewrite nth_uniq. - rewrite -Hi' -Hj' => /eqP ij. by apply val_inj. - by rewrite size_idsA. - by rewrite size_idsA. - by apply uniq_idsA. move=> Hij. by move: (idsA_ids1 Hij). move: (splitP (ord_split j)) => [j' Hj'|j' Hj']. move/eqP. rewrite eq_sym. by move/eqP/idsA_ids1. move=> Htmp. have Hij : i' = j'. apply cols_1_inj. by rewrite -(proj2_sig (ids1 i')) -(proj2_sig (ids1 j')) Htmp. rewrite Hij -Hj' /= in Hi'. exact: val_inj. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel