proposition: Lemma known_port_step x : step_trivIset c en -> step_cond c sp ep en -> known_port c' x = (x \in [set inr p | p in en]) || known_port c x.
proof: Proof. move=> Htriv Hcond. rewrite {1}/known_port /= step_ports_ok // /known_coports step_coports_ok //. move: Htriv Hcond. rewrite /step_cond /step_start_cond /step_end_cond => Htriv /andP [Hsp Hep]. destruct x as [x|y] => /=. by case: imsetP => // [] []. rewrite inE. case: imsetP. move=> [y' Hy' Hyy']. by rewrite (inr_inj Hyy') Hy'. case Hyen: (y \in en) => //. move/imsetP. by rewrite imset_f. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner