fact: Definition gram_neg := gram_neg_rec 0.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup jordan geometry color chromogram) fourcolor(coloring)