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