proposition: Proposition j_geq_0_lt_implies_pred_geq (i j k : nat) : i < j -> k.+1 <= j -> k <= pred j.
proof: Proof. intros l ineq. destruct j. - contradiction (not_lt_n_0 i). - now simpl; apply leq_S_n. Defined.
imports: Basics Spaces.Nat.Core