theorem Std.PRange.Nat.succ_eq {n : Nat} : UpwardEnumerable.succ n = n + 1

theorem Std.PRange.Nat.ClosedOpen.toList_succ_succ {m n : Nat} : { lower := m + 1, upper := n + 1 }.toList = List.map (fun (x : Nat) => x + 1) { lower := m, upper := n }.toList