proposition: Lemma fitp_meet p q x : fitp x p -> fitp x q -> fitp x (meet_part p q).
proof: Proof. elim: p q x => [|sp hp p IHp|hp f1p p IHp|hp f1p f2p p IHp|hp f1p f2p f3p p IHp]; do [move=> q x; rewrite [fitp _ _]/= => /and3P[Esp Ehp] | by case]; do ?[case/andP=> Ef1p | case/andP=> Ef2p | case/andP=> Ef3p] => fit_p; case: q => [|sq hq q|hq f1q q|hq f1q f2q q|hq f1q f2q f3q q] /=; rewrite ?(eqP Esp) ?Esp ?Ehp ?Ef1p ?Ef2p ?Ef3p // => /and3P[Esq Ehq]; do ?[case/andP=> Ef1q | case/andP=> Ef2q | case/andP=> Ef3q] => fit_q; by rewrite (IHp _ _ fit_p fit_q) ?Esq ?Ef1q ?Ef2q ?Ef3q !mem_meet_range. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)