Definition negnatgthmplusnm (n m : nat) : ¬ (m > n + m). Proof. intros. induction n as [ | n IHn ]. - apply isirreflnatgth. - apply natlehtonegnatgth. assert (r := negnatgthtoleh IHn); clear IHn. apply (istransnatleh r (natlthtoleh _ _ (natlthnsn _))). Defined.