proposition: Lemma iter_hub_subn i j : j < nhub -> forall x : G, arity x = nhub -> iter (hub_subn i j) face (iter j face x) = iter i face x.
proof: Proof. move=> ltjn x nFx; rewrite -iterD subnK //; last first. by case: ifP => // _; rewrite ltnW ?ltn_addl. by case: ifP => _ //; rewrite iterD -nFx iter_face_arity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry quiztree part discharge)