n m : m < n <~> 0 < n - m. Proof. induction n as [|n IHn] in m |- *. 1: srapply equiv_iff_hprop; intro; contradiction (not_lt_zero_r _ _). destruct m; only 1: reflexivity. nrefine (IHn m oE _). srapply equiv_iff_hprop. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids