proposition: Lemma size_meet_part p q : size_part (meet_part p q) = size_part p.
proof: Proof. move Dn: (size_part q) => n; move/eqP: Dn. by elim: n p q => [|n IHn] p [] //; case: p => //= *; rewrite IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)