proposition: Lemma coloring_proper_cpring : proper_cpring x0.
proof: Proof. move: memc0_trace_cpring; rewrite /et size_proper_cpring ltnNge head_cpring. by case (behead (cpring x0)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)