∀ (leap : Bool) (month : Std.Time.Month.Ordinal),
  Std.Time.Month.Ordinal.days leap month =
    if ↑month = 2 then if leap = true then 29 else 28
    else
      match Std.Time.Month.Ordinal.monthSizesNonLeap✝ with
      | ⟨months, p⟩ =>
        let index := (Std.Time.Internal.Bounded.LE.sub month 1).toFin Std.Time.Month.Ordinal.days._proof_1✝;
        let idx := Fin.cast ⋯ index;
        months[idx]