Lemma iscotransnatgth (n m k : nat) : n > k -> (n > m) ⨿ (m > k). Proof. intros gnk. induction (isdecrelnatgth n m) as [ p | np ]. - apply ii1. assumption. - apply ii2. induction (isdecrelnatgth m n) as [r|nr]. + apply (istransnatgth _ _ _ r gnk). + assert (e := isantisymmnegnatgth _ _ np nr); clear np nr. induction e. assumption. Defined.