proposition: Lemma hub_subn_hub i j : i < nhub -> hub_subn i j <= nhub.
proof: Proof. move=> ltin; rewrite leq_subLR ltnW //. by have [leji | ltij] := leqP j i; rewrite (ltn_add2r, ltn_addl). 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)