proposition: Theorem sumprod_ok : sumprod_spec vb d.
proof: Proof. move=> a b Hgr. rewrite computed_tree_ok. apply (@message_ok a b #|id'| [::] kv ord0) => //=. + by rewrite card0 subn0 card_sum !card_ord. + rewrite -computed_tree_ok labels_sumprod_down labels_sumprod_up. by apply build_tree_full. + rewrite -computed_tree_ok labels_sumprod_down labels_sumprod_up. by apply build_tree_full. 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