proposition: Lemma fitp_converse p x: exact_fitp x p -> tight_fitp (inv_face2 (edge (face (face x)))) (converse_part p).
proof: Proof. pose t59 h := if h is Pr59 then true else false. have Et59 h T (r1 r2 : T) : (if h is Pr59 then r1 else r2) = if t59 h then r1 else r2. - by case: h. have eEnf (y : G) :edge y = node (face y) by rewrite -{2}[y]De2 edgeK. have fEnne (y : G) : face y = node (node (edge y)) by rewrite eEnf Dn3. move: p => p1 /andP[Ep1 fit_p1]; rewrite /converse_part. set effx := edge (face (face x)). have: let: (h45, q4) := conv_part4 p1 in h45 (arity (edge (face (face (edge (face (face effx))))))) /\ (forall q5, fitp (face (face effx)) q5 -> fitp (face effx) (q4 q5)). - case: p1 fit_p1 {Ep1}; (try by simpl) => h34 h p2. rewrite [fitp _ _]/= => /and3P[Eh34 _ fit_p2]. rewrite fEnne -arity_face nodeK fEnne De2 -eEnf fEnne /effx De2 -eEnf. rewrite -{1}[edge (face x)](iter_face_subn (ltnW (ltnW (pentaG _)))). set n := arity (edge (face x)). rewrite -iterD addnC iterD {1}[Pcons]lock /= !faceK -eEnf -lock. have En: arity (edge (node (edge (face x)))) = n by rewrite -arity_face nodeK. rewrite -[edge x]nodeK arity_face -[node (edge x)]nodeK -fEnne in Eh34. case: p2 fit_p2 => [|s4 f41 p|f41 h45 p|f41 f42 h45 p|h' f1 f2 f3 p]; rewrite /= ?Et59 -/n //. + case/and3P=> Es4 Ef41 _. case (t59 f41); first by rewrite /= En pentaG nodeK Eh34 Es4. by case: s4 in Es4 *; rewrite /= ?pentaG // nodeK En (eqnP Es4) Eh34 ?Ef41. + by case/and4P=> /eqP Dn Ef41 Eh45 _; rewrite En Dn !nodeK eqxx Eh34 Ef41. case/and5P=> /eqP Dn Ef41 Ef42 Eh45 _. by rewrite En Dn !nodeK eqxx Eh34 Ef41 Ef42. case: (conv_part4 p1) => [h45 q4] [Eh45 fit_q4]. move: (drop_part 2 p1) (fitp_drop 2 fit_p1) => p3; rewrite [_ x]/= => fit_p3. have{fit_p3 Eh45}: let: (u, q5) := conv_part5 h45 p3 in u (arity effx) /\ fitp (face (face effx)) q5. - case: p3 fit_p3 => [|u s5 p|h f p|s5 s6 s7 p|h f1 f2 f3 p] //=. by rewrite -/effx Eh45 /= andbT => /and3P[Eu Es5 _]. rewrite -/effx Eh45 !pentaG /= andbT => /andP[Eu]. by rewrite !andbA andbC -!andbA => /andP[]. case: {p3 h45}(conv_part5 h45 p3) => [u q5] [Eu {}/fit_q4]. move: {q4 q5}(q4 q5) => q fit_q. move: (drop_part 3 p1) (fitp_drop 3 fit_p1) => p4; rewrite [_ x]/= => fit_p4. have{fit_p4}: let: (h23, q12) := conv_part12 p4 in h23 (arity (edge (face (face (edge effx))))) /\ (forall q3, fitp effx q3 -> fitp (inv_face2 effx) (q12 q3)). set ef3x := edge (face (face (face x))); set n := arity ef3x. have Ds1: arity (edge (inv_face2 effx)) = arity (edge (face (face ef3x))). by symmetry; rewrite 2!fEnne -arity_face nodeK /ef3x /inv_face2 !De2 -eEnf. have Ds2: edge (face (inv_face2 effx)) = face ef3x. by rewrite /inv_face2 nodeK De2 -[node effx]nodeK /effx -fEnne. rewrite {1}/effx De2; set ef4x := edge (face (face (face (face x)))). have Df21: arity (edge (face (face ef4x))) = arity (edge (iter (n - 2) face ef3x)). + rewrite /ef4x 3!fEnne -/ef3x -arity_face nodeK De2 Dn3 /n. by rewrite -{1}[ef3x]iter_face_arity -(subnKC (pentaG ef3x)) faceK -eEnf. case: p4 fit_p4 => [|s2 s1 p|s1 h12 p|s1 h12 f21 p|h f1 f2 f3 p]; first [ by simpl; split | case: p; rewrite /= ?Et59 ?if_same /=; try by split ]. - move=> h23 f21 _ /and5P[Es2 Es1 Eh23 Ef21 _]; rewrite !Et59 /=. case (t59 f21); first split=> //=. by rewrite //= !pentaG Ds1 Ds2 /ef3x Es1 arity_face Es2 /inv_face2 !nodeK. case: s2 Es2 => //=; rewrite Ds1 Ds2 arity_face -/ef3x -/n => /eqP Dn; rewrite -/ef4x Df21 Dn /= in Ef21; by split; rewrite // Dn eqxx !pentaG /inv_face2 !nodeK Ef21 /ef3x Es1. - rewrite -/ef3x -/ef4x Ds1 Ds2 !pentaG arity_face /= => h23 f21. move=> _ /and5P[/eqP Dn Es1 Eh12 Eh23 /andP[Ef21 _]]. rewrite Df21 /n Dn /= in Ef21. by split; last by rewrite Dn Es1 Eh12 Ef21 /inv_face2 !nodeK. rewrite -/ef3x -/ef4x Ds1 Ds2 !pentaG arity_face /= => h23 f22. move=> _ /and5P[/eqP Dn Es1 Eh12 Ef21 /and3P[Eh23 Ef22 _]]. rewrite Df21 /n Dn /= in Ef22. by split; last by rewrite Dn Es1 Eh12 Ef21 Ef22 /inv_face2 !nodeK. case: {p4}(conv_part12 p4) => [h23 q12] [Eh23 fit_q12]. move: (drop_part 5 p1) (size_drop_part 5 p1) (fitp_drop 5 fit_p1) => p6 Ep6. have{Ep1}Ep6: arity x = 5 + size_part p6 by rewrite Ep6 -(eqP Ep1) subnKC. move=> /= fit_p6. rewrite -2!arity_face {1}/inv_face2 !nodeK Eu /=; apply: {q12}fit_q12. case: p6 fit_p6 Ep6 => //= [_ Ex5 | f31 _ p7 /and3P[Ef31 _]]. by rewrite Eh23 /effx De2 !arity_face Ex5. case: p7 => //= [_ Ex6 | f32 _ p8 /and3P[Ef32 _]]. by rewrite Eh23 /effx De2 !arity_face Ex6 /=. case: p8 => //= [_ Ex7 | f33 _ [] //= /andP[Ef33 _] Ex8]. rewrite !Et59. by do 2?case: ifP; rewrite /= Eh23 /effx De2 !arity_face Ex7 ?Ef31 ?Ef32. by rewrite Eh23 /effx De2 !arity_face Ef31 Ef32 Ef33 Ex8. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)