proposition: Lemma fitp_cmp p x : fitp x p -> forall q, fitp x q = cmp_part p q (fitp x q).
proof: Proof. (elim: p x; first by move=> x _ []) => [sp hp|hp f1p|hp f1p f2p|hp f1p f2p f3p]; move=> p IHp x; rewrite [fitp _ _]/= => /and3P[Es Eh]; do ?[case/andP=> Ef1 | case/andP=> Ef2 | case/andP=> Ef3] => fit_p; case=> //= [sq hq|hq f1q|hq f1q f2q|hq f1q f2q f3q] q; rewrite 1?Epr; rewrite 1?(mem_cmp_range Es) ?(eqnP Es) // (mem_cmp_range Eh) (IHp _ fit_p); rewrite 1?(mem_cmp_range Ef1) 1?(mem_cmp_range Ef2) 1?(mem_cmp_range Ef3); do 1?[case: (cmp_range sp sq) | case: (sp) | case: (sq)] => //=; case: (cmp_range hp hq); rewrite /= ?andbF //; try (case: (cmp_range f1p f1q); rewrite /= ?andbF //); try (case: (cmp_range f2p f2q); rewrite /= ?andbF //); try (case: (cmp_range f3p f3q); rewrite /= ?andbF //); by case (cmp_part p q); rewrite /= ?andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)