Lemma istransnatgth (n m k : nat) : n > m -> m > k -> n > k. Proof. revert m k. induction n as [ | n IHn ]. - intros m k g. induction (negnatgth0n _ g). - intro m. destruct m as [ | m ]. + intros k g g'. induction (negnatgth0n _ g'). + intro k. destruct k as [ | k ]. * intros. apply natgthsn0. * apply (IHn m k). Defined.