proposition: Lemma msg_sz (i1 i2 : id') {k} t : uniq (labels t) -> size (@msg _ _ i1 i2 None k t) = graph t i1 i2.
proof: Proof. move: k t; refine (children_ind _). move=> k [id0 tag0 ch0 up0 down0] /= IH Hun. rewrite !(eq_sym id0). case: ifPn => Hi1. rewrite -(eqP Hi1). rewrite size_flatten /shape. rewrite -map_comp. rewrite (@eq_map _ _ (size \o msg i1 i2 (Some i1)) (pred1 i2 \o node_id)); last first. move=> [id1 ? ? ? ?] /=. by rewrite eqxx (eq_sym id1); case: ifP. rewrite 2!map_comp. rewrite -map_comp. rewrite count_sumn. apply: count_uniq_mem. move /andP: Hun => [_]. by apply: subseq_uniq; exact: subseq_labels. case: ifPn => Hi2. move /andP: Hun => [_ Hun]. rewrite -(eqP Hi2). rewrite size_flatten /shape. rewrite -map_comp. rewrite (@eq_map _ _ (size \o msg i1 i2 (Some i2)) (pred1 i1 \o node_id)); last first. move=> [id1 ? ? ? ?] /=. rewrite eqxx. rewrite (eq_sym id1). case: ifP => [/eqP [Hi12]|]. by rewrite Hi12; case: ifP. by case: ifP. rewrite !map_comp. rewrite -map_comp. rewrite count_sumn. apply: count_uniq_mem. by apply: subseq_uniq Hun; exact: subseq_labels. rewrite (eq_map (msg_none_eq _ _)); [|by rewrite Hi1|by rewrite Hi2]. elim: ch0 => [//| a l IHc] /= in IH Hun *. rewrite size_cat. move: Hun; rewrite cat_uniq => /andP[Hni] /andP [Huna] /andP [Hal Hunl]. have {}IHc: size (flatten [seq msg i1 i2 None i | i <- l]) = has (fun n0 => graph n0 i1 i2) l. apply: IHc. by move=> t' t'l /IH; apply; rewrite in_cons t'l orbT. by move: Hni; rewrite mem_cat => /norP[_ ->]. case Ha: (graph a i1 i2). have Hsz:= f_equal nat_of_bool Ha. rewrite -(IH _ _ Huna) in Hsz; last by rewrite in_cons eqxx. have Hsz': size (msg i1 i2 None a) > 0 by rewrite Hsz. have {Hsz'}[/= Hi1' Hi2']:= msg_nonnil Hsz'. suff ->: size (flatten [seq msg i1 i2 None i | i <- l]) = 0 by rewrite addn0. rewrite size_flatten sumnE big_seq/= big1// => i. rewrite /shape -map_comp => /mapP[x xl] -> /=. apply/msg_nil => /=; apply/orP; left. apply/contra: Hal => Hi1x. apply/hasP; exists i1; last by []. by apply/flattenP; exists (labels x) => //; exact/(map_f labels). rewrite IH => //=; last by rewrite in_cons eqxx. by rewrite Ha /= add0n. 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