proposition: Lemma start_dist_ge0 i : 0 <= start_dist i.
proof: Proof. rewrite /start_dist; case : ifPn => // ?. rewrite mulr_ge0 //; first by apply DegreeDistribution.p0. by rewrite invr_ge0 ler0n. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner