proposition: Lemma Birkhoff5 : Birkhoff_check 4 1.
proof: Proof. by exists 10 [:: Cprog U Y; Cprog 1 U Y; Cprog 2 U Y; Cprog 3 U Y; Cprog 4 U Y; Cprog H 4 Y Y Y]. 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)