proposition: Lemma zrange_dart zp : zpvalid zp -> zrange zp (arity (zdart zp)).
proof: Proof. case: zp => zi pl pr /zvalid_fit; case: zi; rewrite /= /zmove //=. - by rewrite arity_iter_face nFx0 /nhub /hub_range; case: ahub => /=. - by case Dpl: pl; rewrite //= Dnf fitp_catrev; case/and3P. - by rewrite fitp_catrev Dn2 arity_face; case Dpr: pr => //= /and3P[]. - by rewrite fitp_catrev Dne arity_face Dn2; case Dpr: pr => //= /and4P[]. - rewrite -arity_face nodeK. by case Dpl: pl; rewrite //= Dnf fitp_catrev; case/and3P. - by rewrite fitp_catrev Dn2 !arity_face; case Dpr: pr => //= /and3P[]. - by rewrite fitp_catrev De2 Dne !arity_face Dn2; case Dpr: pr => //= /and4P[]. - by case Dpl: pl; rewrite //= fitp_catrev /= Dnf arity_face; case/and4P=> _ Ds _; do !case/andP=> [?]; rewrite (Dfn Ds) !faceK. - by case Dpl: pl; rewrite //= fitp_catrev /= Dnf arity_face; case/and4P=> _ Ds _; do !case/andP=> [?]; rewrite (Dfn Ds) !faceK. - by case Dpl: pl; rewrite //= fitp_catrev /= Dnf arity_face; case/and4P=> _ Ds _; do !case/andP=> [?]; rewrite (Dfn Ds) !faceK. - by case Dpl: pl; rewrite //= fitp_catrev Dnf => /and4P[]. - by case Dpl: pl; rewrite //= fitp_catrev Dnf => /and5P[]. - by case Dpl: pl; rewrite //= fitp_catrev Dnf => /andP[_ /and5P[]]. by case Dpl: pl; rewrite //= fitp_catrev Dnf => /and3P[_ _ /and5P[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)