proposition: Lemma nat_distance_unique_respectful {a b : NatDistance N} : ((=) ==> (=) ==> (=))%signature (nat_distance (nd:=a)) (nat_distance (nd:= b)).
proof: Proof. intros x1 y1 E x2 y2 F. unfold nat_distance, nat_distance_sig. destruct a as [[z1 A]|[z1 A]], b as [[z2 B]|[z2 B]]; simpl. apply (left_cancellation (+) x1). now rewrite A, E, B. destruct (naturals.zero_sum z1 z2). apply (left_cancellation (+) x1). rewrite associativity, A, F, B, E. ring. transitivity 0; intuition. destruct (naturals.zero_sum z1 z2). rewrite commutativity. apply (left_cancellation (+) y1). rewrite associativity, B, <-F, A, E. ring. transitivity 0; intuition. apply (left_cancellation (+) x2). now rewrite A, E, F, B. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals MathClasses.interfaces.orders MathClasses.interfaces.additional_operations