proposition: Lemma head_proper_cpring : proper_cpring -> cpring = [:: node x0, x0 & drop 2 cpring].
proof: Proof. case x0gt2: long_cpring; first by rewrite head_long_cpring. rewrite size_proper_cpring leq_eqVlt -size_long_cpring x0gt2 orbF. rewrite /cpring size_rev size_orbit /orbit => /eqP<-. by move/eqP: x0gt2 => /(canRL (canF_sym nodeK)) <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)