fact: Definition nat_distance `{nd : NatDistance N} (x y : N) := match nat_distance_sig x y with | inl (n↾_) => n | inr (n↾_) => n end.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.varieties.semirings MathClasses.categories.varieties