m n : (m <= n) + (m > n). Proof. induction m as [|m IHm] in n |- *. 1: left; exact _. destruct n. 1: right; exact _. destruct (IHm n). 1: left; exact _. 1: right; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids