@[simp]

theorem Std.PRange.Int.size_rco {a b : Int} : (a...b).size = (b - a).toNat

@[simp]

theorem Std.PRange.Int.size_rcc {a b : Int} : (a...=b).size = (b + 1 - a).toNat

@[simp]

theorem Std.PRange.Int.size_roc {a b : Int} : (a<...=b).size = (b - a).toNat

@[simp]

theorem Std.PRange.Int.size_roo {a b : Int} : (a<...b).size = (b - a - 1).toNat