proposition: Lemma monotonic_edom_step : edom c \subset edom c'.
proof: Proof. case Hcond: (step_trivIset c en && step_cond c sp ep en). move/andP: Hcond => [Htriv Hcond]. rewrite /edom step_edom_ok //. by apply/subsetP => x Hx; rewrite inE Hx orbT. by rewrite /edom step_edom_id. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner