proposition: Lemma fitp_sym p : cmp_part p (mirror_part p) = Psubset -> forall x : G, @exact_fitp (mirror G) x p = exact_fitp x p.
proof: Proof. move=> p_sym x; apply/idP/idP=> /andP[Exp fit_p]. rewrite -{1}[p]mirror_mirror_part fitp_mirror /exact_fitp size_mirror_part. by rewrite Exp (fitp_cmp fit_p) p_sym. by rewrite -fitp_mirror /exact_fitp size_mirror_part Exp (fitp_cmp fit_p) p_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)