proposition: Lemma weighted_count_switch_it len (lam rho : NormalizedDegreeDistribution.L K) c r l : (size lam <= maxdeg -> size rho <= maxdeg -> #|ports (nodes c)| <= len -> #|known_coports c| <= len -> border (conodes c) = set0 -> len * tree_max l.+1 < #|port| -> weighted_count predT (build_graphs lam rho c r l) = r)%nat.
proof: Proof. rewrite /build_graphs. elim: l len lam rho c r => /= [|l IHl] len lam rho c r Hlam Hrho Hp Hcp Hb Hl. rewrite dest_ports_seqs_0. rewrite /image_mem enum_set1 /step_dist_it /=. by rewrite /weighted_count big_seq1. rewrite weighted_count_switch_step //. transitivity (\sum_(t in dest_ports c #|border (nodes c)|) (step_dist_it lam c r t).2). apply eq_bigr => /= t Ht. rewrite tuple_to_partial_enumK. rewrite (surjective_pairing (step_dist_it _ _ _ _)) step_dist_it_1. case/boolP: ((step_dist_it lam c r t).2 == 0) => Hr. rewrite (eqP Hr). rewrite /weighted_count big_map /= big1 //. move=> i _; rewrite switch_step_dist_it_const. by destruct switch_step_dist_it; rewrite mul0r. rewrite (IHl (len * maxdeg.+1)%nat) //. rewrite /switch /=. by apply (ports_conodes_step_it Ht Hr Hlam). rewrite /switch /=. rewrite /known_coports. rewrite /ports part_nodes_step_it. rewrite mulnS. by apply (leq_trans Hp), leq_addr. rewrite /switch /=. by apply border_nodes_step_it. rewrite (leq_ltn_trans _ Hl) //. rewrite /tree_max [in X in (_ <= X)%nat]sum_expr_S mulnDr mulnA. by apply leq_addl. move: (weighted_count_it Hlam). move/(_ def_port c r _ (leqnn _)). rewrite /weighted_count big_map big_enum_in /=. apply. rewrite ltn_subRL. rewrite (leq_ltn_trans _ Hl) //. rewrite /tree_max 2!sum_expr_S mulnDr muln1 mulnA mulnDr muln1 addnA. rewrite (leq_trans _ (leq_addr _ _)) //. rewrite leq_add // leq_mul //. rewrite (leq_trans _ Hp) //. by apply card_border_ports. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner