proposition: Lemma Fgraph_disjoint n0 m0 m1 m2 : m2 \in 'F(m0, n0) -> m2 \in 'F(m1, n0) -> m0 = m1.
proof: Proof. move=> m3m1 m3m2. case/boolP : (m0 == m1) => [/eqP //| m1m2]. exfalso. move: (trivIset_Fgraph_part_fnode n0). move/trivIsetP. move/(_ 'F(m0, n0) 'F(m1, n0)). have m1n1 : n0 \in 'V m0. apply: contraLR m3m1. move/Fgraph_nonempty/eqP => ->. by rewrite in_set0. have m2n1 : n0 \in 'V m1. apply: contraLR m3m2. move/Fgraph_nonempty/eqP => ->. by rewrite in_set0. have H1 : 'F(m0, n0) \in Fgraph_part_fnode n0. apply/imsetP; exists m0 => //; by rewrite FnextE. have H2 : 'F(m1, n0) \in Fgraph_part_fnode n0. apply/imsetP; exists m1 => //; by rewrite FnextE. move/(_ H1 H2) => {H1 H2}. have HF : 'F(m0, n0) != 'F(m1, n0). apply: contra m1m2 => /eqP HF; apply/eqP; exact: Fgraph_injective HF. move/(_ HF) => {HF}. rewrite -setI_eq0 => /set0Pn; apply. exists m2; by rewrite inE m3m1 m3m2. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2