Lemma natgehgthtrans (n m k : nat) : n ≥ m -> m > k -> n > k. Proof. intros gnm gmk. induction (natgehchoice n m gnm) as [ g' | e ]. - apply (istransnatgth _ _ _ g' gmk). - rewrite e. apply gmk. Defined.