proposition: Lemma eqm_loopless : loopless G = loopless G'.
proof: Proof. congr (~~ _ = _); case: G eqG => [d e n f GeK] [e' n' f' G'EK /= eqE eqK _]. by apply: eq_existsb => x; rewrite eqE; apply: eq_fconnect. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)