proposition: Lemma natgthchoice2 (n m : nat) : n > m -> (n > S m) ⨿ (n = (S m)).
proof: Proof. intros g. induction (natgehchoice _ _ (natgthtogehsn _ _ g)) as [ g' | e ]. - apply (ii1 g'). - apply (ii2 e). Defined.
imports: UniMath.Foundations.Sets