proposition: Lemma card_uniq_seq_decr {T : finType} x (s : seq T) h : #|T| - #|s| <= h.+1 -> uniq (x :: s) -> #|T| - #|x :: s| <= h.
proof: Proof. move=> Hh Hun. move /card_uniqP: (Hun) => ->. rewrite /leq -!subnDA in Hh *. rewrite /= addSnnS. rewrite /= in Hun. by move /andP/proj2/card_uniqP: Hun => <-. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo