proposition: Proposition pred_preserves_lt {i n: nat} (p : i < n) m : (n < m) -> (pred n < pred m).
proof: Proof. intro l. apply leq_S_n. destruct (symmetric_paths _ _ (S_predn n i _)). set (k := transitive_lt i n m p l). destruct (symmetric_paths _ _ (S_predn m i _)). assumption. Defined.
imports: Basics Spaces.Nat.Core