proposition: Proposition increasing_geq_n_0 (n : nat) : increasing_geq n 0.
proof: Proof. simple_induction n n IHn. - constructor. - induction IHn. + constructor; now constructor. + constructor; now assumption. Defined.
imports: Basics Spaces.Nat.Core