Lemma nat_eq_or_neq (m n : nat) : (m = n) ⨿ (m ≠ n). Proof. revert m. induction n as [|n N]. - intro m. induction m as [|m _]. + apply ii1. apply idpath. + apply ii2. exact tt. - intro m. induction m as [|m _]. + apply ii2. exact tt. + induction (N m) as [eq|neq]. * apply ii1, maponpaths. assumption. * apply ii2. assumption. Defined.