proposition: Lemma red_qzt_leaf_fit qtl : red_qzt_leaf qtl -> [/\ qzt_proper qtl & forall x : G, zpfit (qstepR x) zp1 -> zpvalid zp1 -> zpfit (qstepR (node x)) zp2 -> zpvalid zp2 -> zpfit (qstepR (node (node x))) zp3 -> zpvalid zp3 -> ~ ~~ qzt_fitl x qtl].
proof: Proof. move=> fit'qtl; split; first by case: qtl fit'qtl. move=> x fit_zp1 zp1ok fit_zp2 zp2ok fit_zp3 zp3ok => /negP[]. elim: qtl fit'qtl => //= q1 q2 q3 qtl IHq; rewrite orbC. case fit_x: (qzt_fitl x qtl) => //; rewrite (contraFF IHq) {fit_x}//. case/and4P=> fit_q3 fit_q2 fit_q1 /and3P[red_q1 red_q2 red_q3]. apply/and3P; split. - by have [<- //|zp1nt] := fitqzp_proper fit_q1; rewrite -fit_zp1 ?fitqzp_fit. - by have [<- //|zp2nt] := fitqzp_proper fit_q2; rewrite -fit_zp2 ?fitqzp_fit. - by have [<- //|zp3nt] := fitqzp_proper fit_q3; rewrite -fit_zp3 ?fitqzp_fit. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)