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