proposition: Lemma exact_fitp_meet p q x : exact_fitp x p -> fitp x q -> exact_fitp x (meet_part p q).
proof: Proof. by rewrite /exact_fitp size_meet_part; case: eqP => // _; exact: fitp_meet. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)