{i n: nat} (p : i < n) m : (n < m) -> (nat_pred n < nat_pred m). Proof. intro l. apply leq_pred'. destruct (symmetric_paths _ _ (nat_succ_pred' n i _)). set (k := transitive_lt i n m p l). destruct (symmetric_paths _ _ (nat_succ_pred' m i _)). assumption. Defined.
Require Import Basics. Require Import Spaces.Nat.Core.