proposition: Lemma step_codom_ok : graph_dom step_conodes = end_port |: graph_dom (conodes c).
proof: Proof. rewrite /step_conodes. destruct Bool.bool_dec => //. rewrite Hcond /=. apply/setP => i. rewrite !inE /ports /=. case: eqP => Hi //=. move/andP: Hcond => [_]. rewrite /step_end_cond inE Hi => /andP [_ Hep]. apply/bigcupP; exists end_node => //. by rewrite !inE eqxx. case: ifP => Hen. by rewrite eq_setSU ?sub1set // !inE orbF. rewrite negb_or -andbA. apply andb_id2l => Hi'. case Hien: (i \in end_node) => /=. symmetry; apply/negP => Hip. by rewrite (trivIset_I1 Htriv Hien) in Hen. rewrite bigcup_setU inE. case Hin: (i \in _) => //. move/bigcupP: Hin Hien => [s]. by rewrite inE => /eqP -> ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner