proposition: Lemma redpart_no_qzt_fitl (y : G) (qa1 qa2 qa3 : qarity) : arity y = qa1 -> arity (node y) = qa2 -> arity (node (node y)) = qa3 -> negb (qzt_fitl y (qzt_get3 qa1 qa2 qa3 qt)).
proof: Proof. move=> Dqa1 Dqa2 Dqa3; have:= fit'qt y. by rewrite /qzt_fit /qzt_fita Dqa1 Dqa2 Dqa3 !qarity_of_qarity !eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)