proposition: Lemma nat_distance_unique {a b: NatDistance N} {x y : N} : nat_distance (nd:=a) x y = nat_distance (nd:=b) x y.
proof: Proof. now apply nat_distance_unique_respectful. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations