Lemma di_neq_i (i x : nat) : i ≠ di i x. Proof. intros. apply nat_nopath_to_neq. intro eq. unfold di in eq. induction (natlthorgeh x i) as [lt|ge]. - induction eq. exact (isirreflnatlth i lt). - induction (!eq); clear eq. exact (negnatgehnsn _ ge). Defined.