{n m : nat} : n <= m -> n <= m. Proof. intro ineq. destruct (@leq_dichotomy n m) as [l | g]. - exact l. - contradiction (lt_irrefl m (lt_lt_leq_trans g ineq)). Defined.
Require Import Basics. Require Import Spaces.Nat.Core.