theorem Nat.mod_sub_eq_of_lt {i j n : Nat} (h : i ≤ j) (h1 : j - i < n) (h2 : i ≤ n) : (j + (n - i)) % n = j - i

theorem Nat.le_lt_sub_lt {i j n : Nat} (h1 : i ≤ j) (h2 : j < n) : j - i < n

theorem Nat.eq_pred_of_le_of_lt_succ {n m : Nat} (h0 : 0 < n) (h1 : n.pred ≤ m) (h2 : m < n) : m = n.pred

theorem Nat.succ_lt_lt {c1 c2 : Nat} (h : 1 + c1 < c2) : c1 < c2

theorem Nat.lt_trans_trans {a b c d : Nat} (h₁ : a < b) (h₂ : b < c) (h₃ : c < d) : a < d

theorem Nat.lt_trans_trans_trans {a b c d e : Nat} (h₁ : a < b) (h₂ : b < c) (h₃ : c < d) (h₄ : d < e) : a < e