Theorems about Time.monthLengths properties

def Lean.Parser.Category.monthLastDayMonthEq : Lean.Parser.Category

Equations

• Lean.Parser.Category.monthLastDayMonthEq = { }

def Verify.MonthLength.Notation.monthLastDayMonthEq.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.monthLastDayMonthEq_________ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.«termMonthLastDayMonthEq%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.monthLastDayMonthEq' : Lean.Parser.Category

Equations

• Lean.Parser.Category.monthLastDayMonthEq' = { }

def Verify.MonthLength.Notation.monthLastDayMonthEq'.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.monthLastDayMonthEq'_________ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.«termMonthLastDayMonthEq'%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.monthLastDayMonthDayEq.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.monthLastDayMonthDayEq : Lean.Parser.Category

Equations

• Lean.Parser.Category.monthLastDayMonthDayEq = { }

def Verify.MonthLength.Notation.monthLastDayMonthDayEq_____ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.«termMonthLastDayMonthDayEq%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.monthIfEq : Lean.Parser.Category

Equations

• Lean.Parser.Category.monthIfEq = { }

def Verify.MonthLength.Notation.monthIfEq.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.monthIfEq_ : Lean.ParserDescr

Equations

• Verify.MonthLength.Notation.monthIfEq_ = Lean.ParserDescr.node `Verify.MonthLength.Notation.monthIfEq_ 1022 (Lean.ParserDescr.const `num)

def Verify.MonthLength.Notation.«termMonthIfEq%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.monthLastDayEqSndLe : Lean.Parser.Category

Equations

• Lean.Parser.Category.monthLastDayEqSndLe = { }

def Verify.MonthLength.Notation.monthLastDayEqSndLe.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.monthLastDayEqSndLe_________ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.«termMonthLastDayEqSndLe%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.monthLastDayEqSnd : Lean.Parser.Category

Equations

• Lean.Parser.Category.monthLastDayEqSnd = { }

def Verify.MonthLength.Notation.monthLastDayEqSnd.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.monthLastDayEqSnd_________ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.Notation.«termMonthLastDayEqSnd%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Verify.MonthLength.monthLengthsOfDate (m : Nat × Nat) (dt : Time.Date) : Prop

Relation of Date to Time.monthLengths list.

Equations

• Verify.MonthLength.monthLengthsOfDate m dt = (m ∈ Time.monthLengths (Time.isLeapYear dt.Year) ∧ m.fst = dt.Month.val ∧ dt.Day.val ≤ m.snd)

def Verify.MonthLength.monthLengths_of_date (dt : Time.Date) : { m : Nat × Nat // Verify.MonthLength.monthLengthsOfDate m dt }

Build relation of Date to Time.monthLengths.

Equations

• One or more equations did not get rendered due to their size.

theorem Verify.MonthLength.monthLengths_days_le (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → (if isleap = true then 29 else 28) ≤ a.snd

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_days_sub_lt (isleap : Bool) (a : Nat × Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → a.snd.fst < a.snd.snd

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_sub_le_31 (isleap : Bool) (a : Nat × Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → a.snd.snd - a.snd.fst ≤ 31

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_sub_of_monthLengths (isleap : Bool) (a : Nat × Nat × Nat) (b : Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → b ∈ Time.monthLengths isleap → a.fst = b.fst → a.snd.snd - a.snd.fst + 1 = b.snd

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_snd_fst_lt (isleap : Bool) (a : Nat × Nat × Nat) : a ∈ Time.monthLastDayAsDayOfYear' isleap → 0 < a.snd.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_month_lt_12_lt (isleap : Bool) (dt : Time.Date) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : a.val.fst < 12) : a.val.snd.fst < if isleap = true then 336 else 335

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_month_1_eq (dt : Time.Date) (isleap : Bool) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : a.val.snd.fst ≤ 31) : 1 = a.val.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_day_of_month_1_eq (dt : Time.Date) (isleap : Bool) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : a.val.fst = 1) : 1 = a.val.snd.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_month_12_eq (dt : Time.Date) (isleap : Bool) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : (if isleap = true then 306 else 305) < a.val.snd.fst) : 12 = a.val.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_month_12_eq' (dt : Time.Date) (isleap : Bool) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : (if isleap = true then 305 else 304) < a.val.snd.fst) : 11 = a.val.fst ∨ 12 = a.val.fst

theorem Verify.MonthLength.monthLastDayAsDayOfYear'_day_of_month_12_eq (dt : Time.Date) (isleap : Bool) (a : { x : Nat × Nat × Nat // x ∈ Time.monthLastDayAsDayOfYear' isleap ∧ x.fst = dt.Month.val }) (h : a.val.fst = 12) : (if isleap = true then 336 else 335) = a.val.snd.fst

theorem Verify.MonthLength.month_11_if_eq {ml : Nat × Nat} (isLeap : Bool) (h : ml ∈ Time.monthLengths isLeap) : ml.fst = 11 → ml.snd = 30