proposition: Lemma zvalid_initr : zvalid p0rl p0rr.
proof: Proof. by move: Ep0r; rewrite -nFx0 -orderSpred /zvalid -zvalid_init; case p0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)