proposition: Lemma eqm_sym G G': G =m G' -> G' =m G.
proof: Proof. by case: G => d e n f EG [] *; apply: EqHypermap => x; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)