n m : n <= m <~> exists k, k + n = m. Proof. srapply equiv_iff_hprop. - apply hprop_allpath. intros [x p] [y q]. pose (r := nat_moveL_nV _ p @ (nat_moveL_nV _ q)^). destruct r. apply ap. apply path_ishprop. - intros p. exists (m - n). apply nat_add_sub_l_cancel, p. - intros [k p]. destruct p. apply leq_add_l. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids