proposition: Proposition pred_gt_implies_lt (i j : nat) : i < pred j -> i.+1 < j.
proof: Proof. intros ineq. assert (H := leq_S_n' _ _ ineq). assert (i < j) as X. { apply (@mixed_trans2 _ (pred j) _); [assumption | apply predn_leq_n]. } destruct (symmetric_paths _ _ (S_predn _ _ X)) in H. assumption. Defined.
imports: Basics Spaces.Nat.Core