trunc_index_min_leq_left@{} (n m : trunc_index) : trunc_index_min n m <= n. Proof. revert n m. refine (trunc_index_ind _ _ _); [ | intros n IHn ]. all: refine (trunc_index_ind _ _ _); [ | intros m IHm ]. all: try exact tt. exact (IHn m). Defined.
Require Import