proposition: Lemma not_red_zpart : ~~ red_zpart.
proof: Proof. have nt_p0l: 1 < size_part p0l. by rewrite 3?ltnW // Dp0l size_rev_part Ep0r -nFx0. have nt_pl: 0 < size_part p0ll by rewrite size_drop_part subn_gt0. have nt_pr: nhub < size_part p0lr. by rewrite size_cat_part Ep0r (leq_add2r _ 1); case: (p0l) nt_p0l. have zp_ok := zvalid_initl. rewrite /red_zpart. elim: nhub p0ll p0lr => // d IHd pl pr in nt_pl nt_pr zp_ok *. pose pl1 := shift_part pr pl; pose pr1 := drop_part 1 pr. have nt_pl1: 0 < size_part pl1 by rewrite size_cat_part ltn_addl. have nt_pr1: d < size_part pr1 by rewrite size_drop_part ltn_subRL. pose zp zi := Zpart zi pl pr; pose zp1 zi := Zpart zi pl1 pr1. pose x := zorg pl; pose y i := iter i face (edge x). have Ezp zi: zdart (zp zi) = zmove zi x by []. have Dzp1 zi zi1: zshiftr zi1 (zp zi) = zp1 zi1. by rewrite /zp zshiftr_eq //; apply: leq_trans nt_pr. have Ezp1 zi: zdart (zp1 zi) = zmove zi (face x). by rewrite -(Dzp1 Zhub) zdart_shiftr. have XEzp1 := Ezp1; rewrite /zp1 in XEzp1. have Dx1 := Ezp1 Zhub; rewrite /= /zmove /= in Dx1. have zp1ok: zpvalid (zp1 Zhub) by rewrite -(Dzp1 Zhub); apply: zpvalid_shiftr. rewrite [Zpart]lock /= -lock Dzp1 /zp1 -!/(zp _) -!/(zp1 _). rewrite negb_or IHd // andbT negb_and -implybE. apply/implyP=> sqt_ok; have [Es Ds _] := qzt_getr_fit sqt_ok. rewrite -{}Ds in sqt_ok *; rewrite qzt_get1_truncate {sqt_ok}//. case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> _ <- /qzt_getr_fit[Esl <- _] /(_ x)IHssl. apply/andP=> -[red_sp red_slp]; case: IHssl => // [_|_||]; rewrite /zpfit. - by rewrite Ezp1 /zmove Dnf. - exact: zdart_shiftl. - exact: zpvalid_shiftl. apply: redpart_no_qzt_fitl; first by rewrite arity_iter_face. by rewrite -(red_popl_spoke_fit zp_ok). by rewrite -(red_popr_spoke_fit zp_ok) // Dn2 arity_face. case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> Eh <- /qzt_getr_fit[Esl <- _] /(_ (y 2))IHhssl. apply/and3P=> -[red_hp red_slp red_sp]; case: IHhssl => //; rewrite /zpfit. - rewrite -(Dzp1 Zhatr) /y /= -Dn2; apply: (@zdart_stepRt (zp Zhatr)) => //. by rewrite /zpfit_top !(Dn2, arity_face) -(red_popr_spoke_fit zp_ok). - by rewrite /qstepR faceK edgeK. - rewrite Dnf -Dn2; apply: (@zdart_stepLt (zp Zhatl))=> //. by rewrite /zpfit_top -arity_face nodeK -(red_popl_spoke_fit zp_ok). apply: redpart_no_qzt_fitl. - by rewrite !arity_face -(red_popr_spoke_fit zp_ok). - by rewrite -arity_face Dnf -Dne De2 -(red_popl_spoke_fit zp_ok). by rewrite Dn2 arity_face -(red_popr_hat_fit zp_ok). move: Es => /(red_popr_spoke_fit zp_ok)/(_ _)/eqP-/implyP; set s := topqa _. case Dpr: pr @s => //= [[]//= h p|h f1 p|h f1 f2 p|h f1 f2 f3 p] Ds; have Es := Dfn Ds; rewrite -/x /= in Ds Es. - case: ifP => // /red_qzt_leaf_fit[]. case/qzt_getr_fit=> Ehr <- /qzt_getr_fit[Eh <- _] /(_ (y 3))IHhhr. apply/andP=> -[red_hr1 red_hr]; case: IHhhr => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /zmove Dnf {1}Es !Dnf -Dn2 Dnf. + by rewrite Ezp /qstepR /zmove Dnf De2 Dnf Dn2. apply: redpart_no_qzt_fitl; first by rewrite /= !arity_face (eqP Ds). by rewrite /= Dnf -(red_popr_hat_fit zp_ok) // Dpr. rewrite -(red_popr_hat_fit zp1ok) //= Dx1 Dn2 -Dnf -(canLR faceK Es). by rewrite !Dne !arity_face. - case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> Ef1 <- /qzt_getr_fit[Eh <- _] /(_ (y 3))IHhf1. apply/andP=> -[red_f1 red_h]; case: IHhf1 => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /zmove De2 /= Dnf (canLR faceK Es) Dnf Dne. + by rewrite Ezp /qstepR /zmove faceK Dnf Dn2. apply: redpart_no_qzt_fitl; first by rewrite /= !arity_face -(eqP Ds). by rewrite /= Dnf -(red_popr_hat_fit zp_ok) // Dpr. rewrite -(red_popl_fan1r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr //=. by rewrite /zmove Dn2 arity_face Dnf. case: ifP => // /red_qzt_leaf_fit[]. case/qzt_getr_fit=> Ehr <- /qzt_getr_fit[Ef1 <- _] /(_ (y 4))IHf1hr. apply/andP=> -[red_hr red_f1]; case: IHf1hr => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /zmove Dnf {1}Es Dnf -Dn2 Dnf. + by rewrite Ezp1 /qstepR /zmove Dnf faceK Dnf. apply: redpart_no_qzt_fitl => //=; first by rewrite /= !arity_face -(eqP Ds). by rewrite -(red_popl_fan1r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr //= /zmove !Dnf. rewrite -(red_popr_hat_fit zp1ok) //= Dx1 Dn2 -Dnf -(canLR faceK Es). by rewrite !Dne !arity_face. - case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> Ef1 <- /qzt_getr_fit[Eh <- _] /(_ (y 3))IHhf1. apply/andP=> -[red_f1 red_h]; case: IHhf1 => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /zmove De2 /= Dnf [in LHS]Es !faceK Dnf Dne. + by rewrite Ezp /qstepR /zmove faceK Dnf Dn2. apply: redpart_no_qzt_fitl; first by rewrite /= !arity_face -(eqP Ds). by rewrite /= Dnf -(red_popr_hat_fit zp_ok) // Dpr. rewrite -(red_popl_fan1r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr //=. by rewrite /zmove Dn2 arity_face Dnf. case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> Ef2 <- /qzt_getr_fit[Hf1 <- _] /(_ (y 4))IHf1f2. apply/andP=> -[red_f2 red_f1]; case: IHf1f2 => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /= /zmove Dnf {1}Es /= !faceK -Dn2 Dnf. + by rewrite Ezp1 /qstepR /= /zmove Dnf faceK Dnf. apply: redpart_no_qzt_fitl => //=; first by rewrite !arity_face -(eqP Ds). by rewrite -(red_popl_fan1r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr // /zmove !Dnf. rewrite -(red_popl_fan2r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr //= /zmove Dn2 !Dnf. by rewrite arity_face. case: ifP => // /red_qzt_leaf_fit[]. case/qzt_getr_fit=> Ehr <- /qzt_getr_fit[Ef2 <- _] /(_ (y 5))IHf2hr. apply/andP=> -[red_hr red_f2]; case: IHf2hr => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /= /zmove Dnf {1}Es Dnf -Dn2 Dnf. + by rewrite Ezp1 /qstepR /= /zmove Dnf faceK Dnf. apply: redpart_no_qzt_fitl => //=; first by rewrite !arity_face -(eqP Ds). by rewrite -(red_popl_fan2r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr // /zmove !Dnf. rewrite -(red_popr_hat_fit zp1ok) //= Dx1 Dn2 -Dnf -(canLR faceK Es). by rewrite !Dne !arity_face. case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> Ef1 <- /qzt_getr_fit[Eh <- _] /(_ (y 3))IHhf1. apply/andP=> -[red_f1 red_h]; case: IHhf1 => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /zmove De2 /= Dnf {1}Es !faceK Dnf Dne. + by rewrite Ezp /qstepR /zmove faceK Dnf Dn2. apply: redpart_no_qzt_fitl; first by rewrite /= !arity_face -(eqP Ds). by rewrite /= Dnf -(red_popr_hat_fit zp_ok) // Dpr. rewrite -(red_popl_fan1r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr //=. by rewrite /zmove Dn2 arity_face Dnf. case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> Ef2 <- /qzt_getr_fit[Ef1 <- _] /(_ (y 4))IHf1f2. apply/andP=> -[red_f2 red_f1]; case: IHf1f2 => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /zmove /= Dnf {1}Es !faceK -Dn2 Dnf. + by rewrite Ezp1 /qstepR /zmove /= Dnf faceK Dnf. apply: redpart_no_qzt_fitl => //=; first by rewrite !arity_face -(eqP Ds). by rewrite -(red_popl_fan1r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr // /zmove !Dnf. rewrite -(red_popl_fan2r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr // /zmove Dn2 !Dnf. by rewrite arity_face. case: ifP => [/red_qzt_leaf_fit[] | _]. case/qzt_getr_fit=> Ef3 <- /qzt_getr_fit[Ef2 <- _] /(_ (y 5))IHf2f3. apply/andP=> -[red_f3 red_f2]; case: IHf2f3 => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 /qstepR /zmove /= Dnf {1}Es !faceK -Dn2 Dnf. + by rewrite Ezp1 /qstepR /zmove /= Dnf faceK Dnf. apply: redpart_no_qzt_fitl => //=; first by rewrite !arity_face -(eqP Ds). by rewrite -(red_popl_fan2r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr // /zmove !Dnf. rewrite -(red_popl_fan3r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr // /zmove Dn2 !Dnf. by rewrite arity_face. case: ifP => // /red_qzt_leaf_fit[]. case/qzt_getr_fit=> Ehr <- /qzt_getr_fit[Ef3 <- _] /(_ (y 6))IHf2hr. apply/andP=> -[red_hr red_f2]; case: IHf2hr => // [_|_|]; rewrite /zpfit. + by rewrite Ezp1 [RHS]Dne -Dnf -Es -Dnf. + by rewrite Ezp1 /qstepR faceK -Dnf Dnf. apply: redpart_no_qzt_fitl => //=; first by rewrite !arity_face -(eqP Ds). by rewrite -(red_popl_fan3r_fit zp1ok) // ?XEzp1 /pl1 ?Dpr // /zmove !Dnf. rewrite -(red_popr_hat_fit zp1ok) //= Dx1 Dn2 -Dnf -(canLR faceK Es). by rewrite !Dne !arity_face. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)