proposition: Lemma fband_nseq x y : cface x y -> forall n, fband (nseq n x) =i fband (nseq n y).
proof: Proof. move=> xFy n z; rewrite !unfold_in. by elim: n => //= n <-; rewrite !(cfaceC z) (same_cface xFy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)