Lemma natlehneggth {n m : nat} : n ≤ m -> ¬ (n > m). Proof. revert m. induction n as [|n N]. - intros m _. exact (negnatgth0n m). - intros m. induction m as [|m _]. + intros r _. exact (negnatlehsn0 n r). + exact (N m). Defined.