proposition: Lemma trivIset_subgraph_succ (simple : simple g) (undirected : symmetric g) (acyclic : acyclic g) n : trivIset ([set n] |: subgraph_succ n).
proof: Proof. apply/trivIsetP => s1 s2. rewrite !inE => /orP[/eqP ->{s1}|]. case/orP => [/eqP ->{s2}|]; first by rewrite eqxx. rewrite (@eq_disjoint1 _ n) //; last by move => ?; rewrite inE. case/imsetP => v Hv -> _; exact: root_notin_subgraph. case/imsetP => m1 Hm1 ->{s1}. case/orP => [/eqP ->|]. rewrite disjoint_sym (@eq_disjoint1 _ n) //; last by move => ?; rewrite inE. move=> _; exact: root_notin_subgraph. case/imsetP => m2 Hm2 ->{s2} s1s2. rewrite !inE in Hm1 Hm2. have m1m2 : m1 != m2 by apply/negP => /eqP m12; rewrite m12 eqxx in s1s2. rewrite -setI_eq0 /subgraph. apply/eqP/setP => x; rewrite !inE Hm1 Hm2 /=. apply/andP; case; case/connectP => p Hp Hp'; subst x. case/connectP => q. have /eq_path -> : except g n =2 fun x y => [&& g y x, y != n & x != n]. by move => x y /=; rewrite exceptE /= undirected andbA andbAC -andbA. rewrite -rev_path => Hq Hpq; move/andP : {Hp Hq} (conj Hp Hq). rewrite -Hpq exceptE -cat_path -exceptE. have : last m1 (p ++ rev (belast m2 q)) = m2. rewrite /rev. case: q Hpq => /=; first by rewrite cats0. by move => qh qt; rewrite catrevE !last_cat. move=> H H0; move/shortenP: H0 H {Hpq} => [] [] //; first by move => /= _ _ _ ?; subst m1; move: m1m2; rewrite eqxx. move => hd tl tl_path tl_uniq _ /= tl_last. move: tl_path => /=; case/andP; rewrite {1}exceptE => /and3P[]; move => m1hd m1n hdn tl_path. move: (acyclic (n :: m1 :: hd :: tl) erefl); apply. rewrite /ucycle cons_uniq tl_uniq andbT inE negb_or eq_sym m1n andTb inE. rewrite negb_or eq_sym hdn andTb (path_except_notin tl_path) andbT /=. by rewrite Hm1 m1hd /= rcons_path (except_path tl_path) /= tl_last undirected. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext