proposition: Lemma reg_ldpc_prop m n : forall (C : reg_ldpc m n), n <> O -> regrho C <> O -> m%:R / n%:R = (reglambda C)%:R / (regrho C)%:R.
proof: Proof. case => /= H lam rho [] Hlam Hrho Hm0 Hrho0. have : (\sum_(m0 : 'I_m) wH (row m0 H) = rho * m)%nat. transitivity (\sum_(m0 < m) rho)%nat. apply eq_bigr => i _; by apply Hrho. by rewrite big_const iter_addn addn0 card_ord. rewrite sum_wH_row => Htmp. have {}Htmp : (lam * n = rho * m)%nat. rewrite -Htmp. transitivity (\sum_(n0 < n) lam)%nat. by rewrite big_const iter_addn addn0 card_ord. apply eq_bigr => i _; exact/esym/Hlam. rewrite -(@eqR_mul2l n%:R); last exact/INR_eq0. rewrite mulRCA mulRV ?INR_eq0' ?mulR1; last exact/eqP. rewrite -(@eqR_mul2l rho%:R); last exact/INR_eq0. rewrite mulRA [in X in _ = X](mulRC rho%:R). rewrite -mulRA (mulRCA rho%:R) mulRV ?INR_eq0' ?mulR1; last exact/eqP. by rewrite -natRM -Htmp natRM mulRC. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext num_occ bigop_ext fdist channel pproba f2 linearcode subgraph_partition tanner tanner_partition hamming binary_symmetric_channel decoding channel_code summary checksum summary_tanner