(n : nat) : increasing_geq n 0. Proof. simple_induction n n IHn. - constructor. - induction IHn. + constructor; by constructor. + constructor; by assumption. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.