proposition: Lemma nat_distance_unique {a b : NatDistance N} : forall x y, @nat_distance _ _ a x y = @nat_distance _ _ b x y.
proof: Proof. intros. unfold nat_distance. destruct (@nat_distance_sig _ _ a x y) as [[z1 E1]|[z1 E1]], (@nat_distance_sig _ _ b x y) as [[z2 E2]|[z2 E2]];simpl. - apply (left_cancellation plus x). path_via y. - rewrite <-(rings.plus_0_r y),<-E2,<-rings.plus_assoc in E1. apply (left_cancellation plus y) in E1. apply naturals.zero_sum in E1. destruct E1;path_via 0. - rewrite <-(rings.plus_0_r x),<-E2,<-rings.plus_assoc in E1. apply (left_cancellation plus x) in E1. apply naturals.zero_sum in E1. destruct E1;path_via 0. - apply (left_cancellation plus y);path_via x. Qed.
imports: HoTT.Classes.orders.naturals HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.naturals