proposition: Lemma dest_dist_out : \sum_(j : {set port} | (i \in j) && trivIset (j |: conodes c)) dest_dist j = 1.
proof: Proof. rewrite /dest_dist. rewrite (partition_big (fun x : {set port} => nth ord0 (enum 'I_U) #|x| ) xpredT) //=. rewrite -[X in _ = X](sum_lambda_pred Hsize_lambda) [X in _ = X]big_mkcond /=. apply eq_bigr => k _. have Hcj: forall j : {set port}, i \in j -> trivIset (j |: conodes c) -> (#|j| < U)%nat. move=> j Hij Htriv. move/subset_leq_card: (conode_outside_ports Hi Hij Htriv). by rewrite cardsCp /U ltnS. case: ifP => /eqP Hk; last first. subst k. rewrite big1 // => j /andP [/andP [Hij Hj] Hk]. case Hj0: (#|j| == 0)%nat. rewrite cards_eq0 in Hj0. by rewrite (eqP Hj0) inE in Hij. move: Hk Hj0. by rewrite (_ : #|j| = Ordinal (Hcj j Hij Hj)) // nth_ord_enum -val_eqE /= => ->. transitivity (\sum_(j : {set port} | [&& #|j| == k, i \in j & trivIset (j |: conodes c)]) lambda`_k.-1 / ('C(#|port|.-1 - #|known_coports c|, k.-1))%:R * 1). apply eq_big => j. rewrite andbC; apply andb_id2r => /andP[ij Htriv]. by rewrite (_ : #|j| = Ordinal (Hcj _ ij Htriv)) // nth_ord_enum. case/andP => /andP[] ij Htriv /eqP jk. case: ifP => Hj. elim (negP Hi). apply/bigcupP. by exists j. by rewrite mulr1 -jk (_ : #|j| = Ordinal (Hcj _ ij Htriv)) // nth_ord_enum. rewrite -big_distrr /= -mulrA -{2}(mulr1 (lambda`_k.-1)). congr GRing.mul. set CE := 'C(_,_)%:R. have unitCE : (CE \is a GRing.unit). apply unitf_gt0. by rewrite ltr0n bin_gt0 -!subn1 subnAC leq_sub2r // -ltnS ltn_ord. rewrite [X in _ * X = _](_ : _ = CE); first by rewrite mulVr. by rewrite /CE -card_nodes3 // sumr_const -cardsE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner