fact: Record plain_cubic : Prop := PlainCubic { plain_cubic_is_plain :> plain; plain_cubic_is_cubic :> cubic }.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)