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