proposition: Lemma dfs_pathP n x y v : #|T| <= #|v| + n -> y \notin v -> reflect (dfs_path v x y) (y \in dfs n v x).
proof: Proof. have dfs_id w z: z \notin w -> dfs_path w z z. by exists [::]; rewrite ?disjoint_has //= orbF. elim: n => [|n IHn] /= in x y v * => le_v'_n not_vy. rewrite addn0 (geq_leqif (subset_leqif_card (subset_predT _))) in le_v'_n. by rewrite predT_subset in not_vy. have [v_x | not_vx] := ifPn. by rewrite (negPf not_vy); right=> [] [p _ _]; rewrite disjoint_has /= v_x. set v1 := x :: v; set a := g x; have sub_dfs := subsetP (subset_dfs n _ _). have [-> | neq_yx] := eqVneq y x. by rewrite sub_dfs ?mem_head //; left; apply: dfs_id. apply: (@equivP (exists2 x1, x1 \in a & dfs_path v1 x1 y)); last first. split=> {IHn} [[x1 a_x1 [p g_p p_y]] | [p /shortenP[]]]. rewrite disjoint_has has_sym /= has_sym /= => /norP[_ not_pv]. by exists (x1 :: p); rewrite /= ?a_x1 // disjoint_has negb_or not_vx. case=> [_ _ _ eq_yx | x1 p1 /=]; first by case/eqP: neq_yx. case/andP=> a_x1 g_p1 /andP[not_p1x _] /subsetP p_p1 p1y not_pv. exists x1 => //; exists p1 => //. rewrite disjoint_sym disjoint_cons not_p1x disjoint_sym. by move: not_pv; rewrite disjoint_cons => /andP[_ /disjointWl->]. have{neq_yx not_vy}: y \notin v1 by apply/norP. have{le_v'_n not_vx}: #|T| <= #|v1| + n by rewrite cardU1 not_vx addSnnS. elim: {x v}a v1 => [|x a IHa] v /= le_v'_n not_vy. by rewrite (negPf not_vy); right=> [] []. set v2 := dfs n v x; have v2v: v \subset v2 := subset_dfs n v [:: x]. have [v2y | not_v2y] := boolP (y \in v2). by rewrite sub_dfs //; left; exists x; [apply: mem_head | apply: IHn]. apply: {IHa}(equivP (IHa _ _ not_v2y)). by rewrite (leq_trans le_v'_n) // leq_add2r subset_leq_card. split=> [] [x1 a_x1 [p g_p p_y not_pv]]. exists x1; [exact: predU1r | exists p => //]. by rewrite disjoint_sym (disjointWl v2v) // disjoint_sym. suffices not_p1v2: [disjoint x1 :: p & v2]. case/predU1P: a_x1 => [def_x1 | ]; last by exists x1; last exists p. case/pred0Pn: not_p1v2; exists x; rewrite /= def_x1 mem_head /=. suffices not_vx: x \notin v by apply/IHn; last apply: dfs_id. by move: not_pv; rewrite disjoint_cons def_x1 => /andP[]. apply: contraR not_v2y => /pred0Pn[x2 /andP[/= p_x2 v2x2]]. case/splitPl: p_x2 p_y g_p not_pv => p0 p2 p0x2. rewrite last_cat cat_path -cat_cons lastI cat_rcons {}p0x2 => p2y /andP[_ g_p2]. rewrite disjoint_cat disjoint_cons => /and3P[{p0}_ not_vx2 not_p2v]. have{not_vx2 v2x2} [p1 g_p1 p1_x2 not_p1v] := IHn _ _ v le_v'_n not_vx2 v2x2. apply/IHn=> //; exists (p1 ++ p2); rewrite ?cat_path ?last_cat -?p1_x2 ?g_p1 //. by rewrite -cat_cons disjoint_cat not_p1v. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)