proposition: Theorem connected_step : partial_connected c -> partial_connected c'.
proof: Proof. move => Hc x y Hx Hy. case Hcond: (step_trivIset c en && step_cond c sp ep en); last first. rewrite /known_port /known_coports /= step_nodes_id // step_conodes_id // in Hx Hy. case: (@Hc x y) => // p [b1 [b2 Hp]]. exists p, b1, b2. rewrite (eq_path (graph_rel_irrel _)) //. by rewrite /= step_nodes_id // step_conodes_id // step_edges_id. move/andP: Hcond => [Htriv Hcond]. case Hx': (known_port c x). case Hy': (known_port c y). case: (@Hc x y) => // p [b1 [b2 /andP [Hp Hl]]]. exists p; exists b1; exists b2. rewrite Hl andbT. by apply (sub_path monotonic_step_rel). by apply connected_step_out. case Hy': (known_port c y). destruct(connected_step_out Hc Htriv Hcond Hy Hx Hy' Hx') as [p [b1 [b2 Hp]]]. exists (map (@flip port) (rev (belast (y,b1) p))); exists (~~b2), (~~b1). move/andP: Hp => [Hp Hl]. apply/andP; split. rewrite (_ : (x,~~b2) = last (flip (y,b1)) (map (@flip port) p)). by apply flip_seq_path. by rewrite last_map (eqP Hl). rewrite -/(flip (x,b2)) last_map. destruct p => /=. by rewrite -(eqP Hl). by rewrite rev_cons last_rcons. case Hxy: (x == y). exists [::], true, true. by rewrite (eqP Hxy) eqxx. exists [:: (y,true)], false, true. move: Hx Hy Hxy; rewrite known_port_step // known_port_step //. rewrite Hx' Hy' !orbF. move/imsetP=> [x' Hxen] ->. move/imsetP=> [y' Hyen] -> /= Hxy'. rewrite eqxx !andbT. apply/existsP; exists en. rewrite Hxen Hyen en_in_step_conodes //=. by move/negbT: Hxy'; apply/contra => /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner