proposition: Lemma tn_tree_eqP k : Equality.axiom (@tn_tree_eq_bool k).
proof: Proof. move=> x. pose d := depth x. have Hd: depth x <= d by []. clearbody d. elim: d k x Hd => [|d IHd] k x Hd y. by destruct x; rewrite ltn0 in Hd. case Heq: (tn_tree_eq_bool x y); constructor. case: x y Hd Heq => [id0 tag0 ch0 up0 down0] [id1 tag1 ch1 up1 down1] /= Hd. do! move/andP=>[]; do! move/eqP->; move=> Hlen Hall. congr Node. move: Hd ch1 Hall Hlen; clear -IHd. elim: ch0 => [| a chld0 IH] Hd [] // b chld1 /= /andP[ab Hch]. rewrite eqSS => Hlen. rewrite /= big_cons in Hd. congr (_ :: _). apply/IHd => //. refine (leq_ltn_trans _ Hd). by rewrite leq_max leqnn. apply IH => //. by rewrite (leq_ltn_trans _ Hd) // leq_maxr. move=> ?; subst y. case: x Hd Heq => /= ? ? children ? ? Hd. rewrite !eqxx /= => /negP; apply. clear -IHd Hd. elim: children Hd => //= a ch0 IH. rewrite big_cons => Hd. rewrite IH ?andbT. apply /IHd => //. refine (leq_ltn_trans _ Hd). by rewrite leq_max leqnn. by rewrite (leq_ltn_trans _ Hd) // leq_maxr. 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