trunc_index_min_swap@{} n m : trunc_index_min n m = trunc_index_min m n. Proof. revert m. simple_induction n n IHn; intro m. { symmetry. apply trunc_index_min_minus_two. } simple_induction m m IHm. 1: reflexivity. cbn; apply ap, IHn. Defined.
Require Import