Lemma natgthchoice3 (n m : nat) : n > m -> (n > (m + 1)) ⨿ (n = (m + 1)). Proof. intros g. induction (natgehchoice _ _ (natgthtogehp1 _ _ g)) as [ g' | e ]. - apply (ii1 g'). - apply (ii2 e). Defined.