proposition: Lemma no_cycle_in_known_ports (n : 'I_(#|port|*4)%nat) : forall px : (n.+1).-tuple ((port + port) * bool)%type, path.cycle (graph_rel (step c p i.1 i.2)) px -> uniq px -> all (fun x : graph_node port * bool => known_port c x.1) px = false.
proof: Proof. move=> [px Hpx] /= Hcy Hun. apply/allP => /= Hin. move/'forall_forallP : Hc => /(_ n (Tuple Hpx)). rewrite /ucycleb Hun andbT /= => /negP; apply. rewrite /path.cycle /= in Hcy *. destruct px as [|a px] => //. rewrite (@eq_path_in _ _ (graph_rel c) (fun x => known_port c x.1)) // in Hcy; last first. rewrite -rcons_cons all_rcons Hin. by apply/allP. by rewrite in_cons eqxx. move=> /= x y Hkx Hky. destruct x as [x xb], y as [y yb]. rewrite /known_port !unfold_in /= in Hkx Hky. destruct x as [x|x], y as [y|y], xb, yb => //=. - by rewrite /step_nodes Hsc /step_trivIset Htriv. - by apply eq_edom_edges_inout. - by apply eq_edom_edges_inout. - rewrite step_conodes_ok //. apply/existsP. case: ifP => /existsP. move=> [s] /andP[Hsco Hs]. exists s. by rewrite inE Hsco Hs orbT. move=> Hex [s Hs]; apply Hex. exists s. move/andP: Hs => [Hsco Hs]. rewrite Hs andbT. move: Hsco. rewrite !inE => /orP [|] // Hsco. move/andP: Hs => []. rewrite (eqP Hsco) => Hxi2 _. by apply (trivIset_I1 Htriv Hxi2). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner