proposition: Lemma wf_visit e x : wf_env e -> (forall y, num e y < sn e -> gconnect y x) -> x \notin visited e -> wf_env (visit x e).
proof: Proof. move=> e_wf x_connected xNvisited. constructor=> [|y|y|] //=; rewrite ?inE ?ffunE/=. - exact: sub_gsccs. - rewrite visited_visit cardsU1 xNvisited; case: ifPn => // _. by rewrite num_lt_V// ltnS => /ltnW. - have [->|] := altP (y =P x); last by rewrite num_sccs. rewrite -num_sccs// eq_sym !gtn_eqF ?num_gt_V//. by rewrite (@leq_trans #|x |: visited e|) ?max_card// cardsU1 xNvisited. move=> y z; rewrite !ffunE/=. have sub_visit : visited e \subset visited (visit x e). by apply/subsetP => ?; rewrite visited_visit !inE orbC => ->. have [{y}->|neq_yx] := altP eqP; have [{z}->|neq_zx]//= := altP eqP. + by rewrite num_lt_card//; case: ltngtP. + move=> /andP[/leq_ltn_trans lt/lt]. by rewrite num_lt_card//; apply: x_connected. + by rewrite num_lt_card//; apply: le_connect. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors