proposition: Lemma trivIset_subgraph_succ2_D1_helper (Hg : simple g) m n1 n2 m1 m2 v (l k k' : seq V) (n1n2 : n1 != n2) (mn1 : g m n1) (mn2 : g m n2) (n1m1 : g n1 m1) (n2m2 : g n2 m2) (m2m : m2 != m) (Hunk : uniq (m2 :: k')) (k'k : subpred (mem k') (mem k)) (Hk' : path (except g n2) m2 k') (Hlast : v = last m1 l) (Hkast : v = last m2 k') : 0 < size l.
proof: Proof. case: l Hlast => //= vm1; subst m1. exfalso. suff : ucycle g [:: n1, m, n2, m2 & k'] by apply acyclic_g. apply/andP; split. rewrite /= symmetric_g mn1 /= mn2 /= n2m2 /= rcons_path. by rewrite (except_path Hk') /= -Hkast symmetric_g. rewrite -(cat1s n1) -(cat1s m) -(cat1s n2) 2!catA cat_uniq Hunk andbT. apply/andP; split. by rewrite /= !inE negb_or eq_sym (simple_neg Hg) //= n1n2 /= (simple_neg Hg). rewrite /= !inE /= !negb_or /=; apply/andP; split. rewrite m2m andTb andbC (simple_neg Hg) //= 1?symmetric_g //. apply/eqP => ?; subst m2. suff : ucycle g [:: m; n2; n1] by apply acyclic_g. apply/andP; split; first by rewrite /= mn2 n2m2 symmetric_g mn1. rewrite /= !inE negb_or /= andbT (simple_neg Hg mn2) /= eq_sym. by rewrite eq_sym (simple_neg Hg) //= eq_sym. apply/hasP; case=> x Hx /=. rewrite !inE; case/orP => [/eqP xn1|]. move: Hx; rewrite {}xn1 {x} => Hx. case/splitPr : Hx => k1 k2 in Hk' Hunk k'k Hkast. suff : ucycle g [:: n1, m, n2, m2 & k1] by apply acyclic_g. apply/andP; split. rewrite /path.cycle rcons_path /= symmetric_g mn1 /= mn2 /= n2m2 /=. move: Hk'; rewrite cat_path => /andP[/except_path -> /=]. by rewrite exceptE /= => /andP[/andP[]]. move: (Hunk). rewrite -cat_cons cat_uniq => /andP [] m2k1 _. rewrite -(cat1s n1) -(cat1s m) -(cat1s n2) 2!catA cat_uniq m2k1 andbT. apply/andP; split. by rewrite /= !inE negb_or /= eq_sym (simple_neg Hg) //= n1n2 (simple_neg Hg). apply/hasP; case => x. rewrite inE. case/orP => [/eqP ->{x}|xk1]. rewrite /= !inE /= (eq_sym m2 n2)(negbTE (simple_neg Hg n2m2)). rewrite (negbTE m2m) /= orbF => /eqP m'2n1. by move: Hunk; rewrite /= mem_cat m'2n1 inE eqxx orbCA. rewrite /= !inE. case/orP => [/eqP xn1|]. move: Hunk; by rewrite -xn1 /= -cat_rcons cat_uniq rcons_uniq xk1 /= andbF. case/orP => /eqP ?; subst x. case/splitPr : xk1 => k11 k12 in Hk' Hunk k'k Hkast m2k1. suff : ucycle g [:: m, n2, m2 & k11] by apply acyclic_g. move: Hk'; rewrite cat_path => /andP[Hk' _]; move: Hk'. rewrite -[in X in X -> _](cat1s m) catA cat_path cats1 => /andP[Hk' _]. move: Hunk; rewrite -cat_cons cat_uniq; case/andP => Hunk _; move: Hunk. rewrite -[in X in X -> _](cat1s m2) -[in X in X -> _](cat1s m) 2!catA. rewrite cat_uniq cats1 => /and3P[Hunk _ _]. exact: uniq_path_ucycle_extend_1 Hk' Hunk. by move: Hk'; rewrite cat_path => /andP[/path_except_notin]; rewrite xk1. case/orP => [/eqP xm|/eqP xn2]. move: Hx; rewrite {}xm {x} => xk'. case/splitPr : xk' => k1 k2 in Hk' Hunk k'k Hkast. suff : ucycle g [:: m, n2, m2 & k1] by apply acyclic_g. move: Hk'; rewrite -[in X in X -> _](cat1s m) catA cat_path cats1 => /andP[Hk' _]. move: Hunk; rewrite -[in X in X -> _](cat1s m2) -[in X in X -> _](cat1s m) 2!catA cat_uniq cats1 => /andP[Hunk _]. exact: uniq_path_ucycle_extend_1 Hk' Hunk. by move/path_except_notin : Hk'; rewrite -xn2 Hx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext