proposition: Lemma updateP8f2 h f1 f3 : part_update (fun r => Pcons8 h f1 r f3) Pfan2.
proof: Proof. by move=> r p; split=> //= g x /and5P[-> -> -> -> ->]; split=> // r' ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)