∀ {α : Type u} [inst : Std.Rxc.HasSize α] [inst_1 : Std.PRange.Least? α] (r : Std.Ric α),
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some least => Std.Rxc.HasSize.size least r.upper