trunc_index_leq@{} (m n : trunc_index) : Type0 := match m, n with | -2, _ => Unit | m'.+1, -2 => Empty | m'.+1, n'.+1 => trunc_index_leq m' n' end. Existing Class trunc_index_leq. Notation "m <= n" := (trunc_index_leq m n) : trunc_scope. Global Instance trunc_index_leq_minus_two_n@{} n : -2 <= n := tt. Global Instance trunc_index_leq_succ@{} n : n <= n.+1. Proof. by induction n as [|n IHn] using trunc_index_ind. Defined.
Require Import