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

theorem Std.Legacy.Range.size_step_1 (start stop : Nat) : [start:stop].size = stop - start