proposition: Lemma seq_full {A:finType} (s : seq A) a : #|A| - #|s| <= 0 -> a \in s.
proof: Proof. move=> Hh. have Hs: finset (mem s) = [set: A]. apply/eqP. rewrite eqEcard subsetT /=. rewrite cardsT cardsE. by rewrite /leq subn0 in Hh. by move/setP : Hs => /(_ a); rewrite !inE. 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