Lemma natneq_iff_neq n m : ¬ (n = m) <-> n ≠ m. Proof. revert m. induction n as [|n N]. - intro m. induction m as [|m _]. + apply logeq_both_false. * intro n. exact (n (idpath 0)). * simpl. exact (idfun ∅). + apply logeq_both_true. * apply negpaths0sx. * simpl. exact tt. - intro m. induction m as [|m _]. + apply logeq_both_true. * apply negpathssx0. * simpl. exact tt. + split. * intro ne. apply (pr1 (N m)). intro r. exact (ne (maponpaths S r)). * intro neq. apply noeqinjS. apply (pr2 (N m)). exact neq. Defined.