{a b : NatDistance N} : forall x y, @nat_distance _ _ a x y = @nat_distance _ _ b x y. 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.
Require Import Require Import