n m l : (n | m) -> (n | m + l) -> (n | l). Proof. intros [x p] [y q]. exists (y - x). lhs nrapply nat_dist_sub_r. apply nat_moveR_nV. lhs nrapply q. lhs nrapply nat_add_comm. exact (ap _ p^). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes