Definition nat_tree : Tree. Proof. refine (make nat nat_dist _ _ _ _ _). { intro m. induction m as [|m IHm]. { reflexivity. } { rewrite nat_dist_S. assumption. } } { apply nat_dist_anti. } { apply nat_dist_symm. } { apply nat_dist_trans. } { intros m n e. Set Printing All. assert (d := natneqchoice _ _ (nat_nopath_to_neq e)); clear e. destruct d as [h|h]. { exists (S n). { split. { apply nat_dist_gt. exact h. } { destruct (natgthorleh (S n) n) as [_|j]. { clear h. induction n as [|n IHn]. { reflexivity. } { apply IHn. } } { apply fromempty. clear h. contradicts j (negnatSleh n). }}} } { exists (n - 1). { split. { assert (a := natltminus1 m n h). assert (b := natlthtoleh m n h). assert (c := nat_dist_le _ _ a). assert (d := nat_dist_le _ _ b). rewrite c, d; clear c d. rewrite natminusminusassoc. simpl. change (1 + (n - (1+m)) = n - m). rewrite (natpluscomm 1 m). rewrite <- natminusminusassoc. rewrite natpluscomm. apply (minusplusnmm (n-m) 1). apply (natminusplusltcomm m n 1). { assert(e := natleh0n m). assert(f := natlehlthtrans _ _ _ e h). exact (natlthtolehsn _ _ f). } { exact a. } } { assert (a := natleh0n m). assert (b := natlehlthtrans _ _ _ a h). assert (c := natlthtolehsn _ _ b). exact (nat_dist_minus 1 n c). } } } } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Nat. Import UniMath.MoreFoundations.Nat.Discern. Require Import UniMath.MoreFoundations.Notations.