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