proposition: Lemma orderEord f x : order f x = order_ord f x.
proof: Proof. Abort. Definition orbit_ord f x := traject f x (order_ord f x). Lemma orbitEord f x : orbit f x = orbit_ord f x. Abort. Definition connect_ord (e : rel 'I_n) x y := y \in dfs (sseq e) n [::] x. Lemma connectEord (e : rel 'I_n) : connect e =2 connect_ord e. Proof. move => x y; rewrite (eq_connect (eq_sseq e)); apply: connectEdfs. by rewrite card_ord. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)