proposition: Proposition leq_equivalent (n m : nat) : n <= m <-> increasing_geq m n.
proof: Proof. split. - intro ineq. induction ineq. + constructor. + apply increasing_geq_S_n in IHineq; constructor; assumption. - intro a. induction a. + constructor. + exact (leq_S' _ _ _). Defined.
imports: Basics Spaces.Nat.Core