theorem Std.Range.size_stop_le_start (r : Range) : r.stop ≤ r.start → r.size = 0

theorem Std.Range.size_step_1 (start stop : Nat) : { start := start, stop := stop, step_pos := ⋯ }.size = stop - start