proposition: Lemma cpring0 b : @cpring cpmap0 b = [:: ~~ b; b].
proof: Proof. by case: b; apply: cpring_def. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)