Definition nat_dist_trans x y z : nat_dist x z ≤ nat_dist x y + nat_dist y z. Proof. intros. induction (natleorle x y) as [r|s]. { rewrite (nat_dist_le _ _ r). induction (natleorle y z) as [t|u]. { assert (u := istransnatgeh _ _ _ t r). rewrite (nat_dist_le _ _ t). rewrite (nat_dist_le _ _ u). apply (natlehandplusrinv _ _ x). rewrite (minusplusnmm _ _ u). rewrite (natpluscomm _ x). rewrite <- natplusassoc. rewrite (natpluscomm x). rewrite (minusplusnmm _ _ r). rewrite (natpluscomm y). rewrite (minusplusnmm _ _ t). apply isreflnatleh. } { rewrite (nat_dist_ge _ _ u). induction (natleorle x z) as [p|q]. { rewrite (nat_dist_le _ _ p). apply (natlehandplusrinv _ _ x). rewrite (minusplusnmm _ _ p). rewrite natpluscomm. rewrite <- natplusassoc. rewrite (natpluscomm x). rewrite (minusplusnmm _ _ r). apply (natlehandplusrinv _ _ z). rewrite natplusassoc. rewrite (minusplusnmm _ _ u). apply (istransnatleh (m := y+z)). { apply natlehandplusr. exact u. } { apply natlehandplusl. exact u. } } { rewrite (nat_dist_ge _ _ q). apply (natlehandplusrinv _ _ z). rewrite (minusplusnmm _ _ q). rewrite natplusassoc. rewrite (minusplusnmm _ _ u). rewrite natpluscomm. apply (natlehandplusrinv _ _ x). rewrite natplusassoc. rewrite (minusplusnmm _ _ r). apply (istransnatleh (m := x+y)). { apply natlehandplusl. assumption. } { apply natlehandplusr. assumption. } } } } { rewrite (nat_dist_ge _ _ s). induction (natleorle z y) as [u|t]. { assert (w := istransnatleh u s). rewrite (nat_dist_ge _ _ w). rewrite (nat_dist_ge _ _ u). apply (natlehandplusrinv _ _ z). rewrite (minusplusnmm _ _ w). rewrite natplusassoc. rewrite (minusplusnmm _ _ u). rewrite (minusplusnmm _ _ s). apply isreflnatleh. } { rewrite (nat_dist_le _ _ t). induction (natleorle x z) as [p|q]. { rewrite (nat_dist_le _ _ p). apply (natlehandplusrinv _ _ x). rewrite (minusplusnmm _ _ p). apply (natlehandpluslinv _ _ y). rewrite (natplusassoc (x-y)). rewrite <- (natplusassoc y). rewrite (natpluscomm y (x-y)). rewrite (minusplusnmm _ _ s). apply (natlehandplusrinv _ _ y). rewrite (natplusassoc x). rewrite (natplusassoc _ x y). rewrite (natpluscomm x y). rewrite <- (natplusassoc _ y x). rewrite (minusplusnmm _ _ t). rewrite (natpluscomm z x). rewrite <- (natplusassoc x). rewrite (natplusassoc y). rewrite (natpluscomm z y). rewrite <- (natplusassoc y). apply (natlehandplusr _ _ z). apply (istransnatleh (m := x+y)). { apply natlehandplusr. assumption. } { apply natlehandplusl. assumption. } } { rewrite (nat_dist_ge _ _ q). apply (natlehandplusrinv _ _ z). rewrite (minusplusnmm _ _ q). apply (natlehandpluslinv _ _ y). rewrite (natplusassoc (x-y)). rewrite <- (natplusassoc y). rewrite (natpluscomm y (x-y)). rewrite (minusplusnmm _ _ s). apply (natlehandplusrinv _ _ y). rewrite (natplusassoc x). rewrite (natplusassoc _ z y). rewrite (natpluscomm z y). rewrite <- (natplusassoc _ y z). rewrite (minusplusnmm _ _ t). rewrite (natpluscomm y x). rewrite (natplusassoc x). apply natlehandplusl. apply (istransnatleh (m := z+y)). { apply natlehandplusr. assumption. } { apply natlehandplusl. assumption. } } } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.