proposition: Lemma rlinkFr y1 y2 : cface y1 y2 -> forall x, rlink x y1 = rlink x y2.
proof: Proof. by move=> y1Fy2 x; rewrite /rlink !(cfaceC (edge x)) (same_cface y1Fy2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)