Definition istransnatleh {n m k : nat} : n ≤ m -> m ≤ k -> n ≤ k. Proof. intros r s. apply negnatgthtoleh. assert (b := natlehneggth r); clear r. assert (c := natlehneggth s); clear s. intro r. induction (iscotransnatgth _ m _ r) as [t|t]. - contradicts b t. - contradicts c t. Defined.