proposition: Lemma updateP7h f1 f2 : part_update (fun r => Pcons7 r f1 f2) Phat.
proof: Proof. by move=> r p; split=> //= g x /and3P[-> -> ->]; split=> // r' ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)