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