proposition: Theorem Birkhoff (r : seq G) : size r <= 5 -> scycle rlink r -> nontrivial_ring (size r == 5) r = false.
proof: Proof. elim: {1 3}5 (leqnn 5) => [|n IHn] n_lt5 in r *. case: r => // _ _; rewrite /nontrivial_ring [fcard _ _]eq_card0 // => x. by rewrite !inE andbF. move/(_ (ltnW n_lt5)) in IHn; rewrite leq_eqVlt => /predU1P[]; last exact: IHn. move=> sz_r Ur; apply: (Birkhoff_valid _ _ Ur sz_r). move {r Ur sz_r} => r Ur r_le_n; rewrite -(IHn r r_le_n) //. by rewrite eqn_leq andbC leqNgt (leq_trans _ n_lt5). have [*] := And4 Birkhoff2 Birkhoff3 Birkhoff4 Birkhoff5. rewrite sz_r; case: n sz_r n_lt5 {IHn}; last by do 4![case=> //]. by case: r Ur => [|x []]; rewrite /scycle //= /rlink cfaceC bridgeless_cface. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)