(n m : nat) : n <= m <-> increasing_geq m n. Proof. split. - intro ineq. induction ineq. + constructor. + apply increasing_geq_S_n in IHineq; constructor; assumption. - intro a. induction a. + constructor. + exact (leq_succ_l _). Defined.
Require Import Basics. Require Import Spaces.Nat.Core.