20.18. 范围🔗

range 表示某种类型的一系列连续元素，从下限到上限。边界可以是开放的，在这种情况下，边界值不是范围的一部分；也可以是封闭的，在这种情况下，边界值是范围的一部分。任一边界都可以省略，在这种情况下，范围在相应方向上无限延伸。

范围具有专用语法，由起点 ... 和终点组成。起始点可以是 *（表示无限向下延续的范围），也可以是术语（表示具有特定起始值的范围）。默认情况下，范围是左闭的：它们包含它们的起点。尾随 < 表示该范围是左开的并且不包含其起点。结束点可以是 *（在这种情况下，范围无限向上），也可以是一个术语，表示具有特定结束值的范围。默认情况下，范围是右开的：它们不包含结束点。终点可能会带有<前缀，表示它是右开的；这是默认值，不会改变含义，但可能更容易阅读。它还可能带有 = 前缀，以指示该范围是右闭的并包含其结束点。

Ranges of Natural Numbers

包含数字 3 到 6 的范围可以用多种方式编写：

[3, 4, 5, 6]#eval (3...7).toList

[3, 4, 5, 6]

[3, 4, 5, 6]#eval (3...=6).toList

[3, 4, 5, 6]

[3, 4, 5, 6]#eval (2<...=6).toList

[3, 4, 5, 6]

Live ↪

Finite and Infinite Ranges

该范围无法转换为列表，因为它是无限的：

#eval failed to synthesize instance of type class
  Std.Rxi.IsAlwaysFinite Nat

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.(3...*).toList

左闭右无界范围的有限性由 Std.Rxi.IsAlwaysFinite 实例的存在来指示，而 Nat 则不存在该实例。 Std.Rco 是这些范围的类型，名称 Std.Rxi.IsAlwaysFinite 表明它确定所有右无界范围的有限性。

failed to synthesize instance of type class
  Std.Rxi.IsAlwaysFinite Nat

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

尝试枚举负整数会导致类似的错误，这次是因为无法确定最小元素：

#eval failed to synthesize instance of type class
  Std.PRange.Least? Int

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.(*...(0 : Int)).toList

failed to synthesize instance of type class
  Std.PRange.Least? Int

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

有限类型中的无界范围表示范围扩展到该类型的最大元素。由于 UInt8 有 256 个元素，因此该范围包含 253 个元素：

253#eval ((3 : UInt8)...*).toArray.size

Live ↪

syntaxRange Syntax

该范围为左闭、右开，表示Std.Rco：

term ::= ...
    | `a...b` is the range of elements greater than or equal to `a` and less than `b`.
See also `Std.Rco`.
term...term

该范围为左闭、右开，表示Std.Rco：

term ::= ...
    | `a...<b` is the range of elements greater than or equal to `a` and less than `b`.
See also `Std.Rco`.
term...<term

该范围为左闭、右闭，表示Std.Rcc：

term ::= ...
    | `a...=b` is the range of elements greater than or equal to `a` and less than or equal to
`b`. See also `Std.Rcc`.
term...=term

该范围是左闭右无限，表示 Std.Rci：

term ::= ...
    | `a...*` is the range of elements greater than or equal to `a`. See also `Std.Rci`. term...*

该范围有左开、右开，表示Std.Roo：

term ::= ...
    | `a<...b` is the range of elements greater than `a` and less than `b`.
See also `Std.Roo`.
term<...term

该范围有左开、右开，表示Std.Roo：

term ::= ...
    | `a<...<b` is the range of elements greater than `a` and less than `b`.
See also `Std.Roo`.
term<...<term

该范围为左开、右闭，表示Std.Roc：

term ::= ...
    | `a<...=b` is the range of elements greater than `a` and less than or equal to `b`.
See also `Std.Roc`.
term<...=term

该范围为左开、右无限，表示 Std.Roi：

term ::= ...
    | `a<...*` is the range of elements greater than `a`. See also `Std.Roi`. term<...*

该范围为左无穷、右开，表示 Std.Rio：

term ::= ...
    | `*...b` is the range of elements less than `b`. See also `Std.Rio`. *...term

该范围为左无穷、右开，表示 Std.Ric：

term ::= ...
    | `*...<b` is the range of elements less than `b`. See also `Std.Rio`. *...<term

该范围是左无穷、右闭的，表示 Std.Ric：

term ::= ...
    | `*...=b` is the range of elements less than or equal to `b`. See also `Std.Ric`. *...=term

该范围两边都是无穷大，表示 Std.Rii：

term ::= ...
    | `*...*` is the range that is unbounded in both directions. See also `Std.Rii`. *...*

20.18.1. 范围类型🔗

structure

Std.Rco.{u} (α : Type u) : Type u
Std.Rco.{u} (α : Type u) : Type u

A range of elements of α with a closed lower bound and an open upper bound.

a...b or a...<b is the range of all values greater than or equal to a : α and less than b : α. This is notation for Rco.mk a b.

Constructor

Std.Rco.mk.{u}

Fields

lower : α

The lower bound of the range. lower is included in the range.

upper : α

The upper bound of the range. upper is not included in the range.

def

Std.Rco.iter.{u_1} {α : Type u_1} (r : Std.Rco α) : Std.Iter α
Std.Rco.iter.{u_1} {α : Type u_1}
  (r : Std.Rco α) : Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Rco.toArray.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Rco α) : Array α
Std.Rco.toArray.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rco α) : Array α

Returns the elements of the given left-closed right-open range as an array in ascending order.

def

Std.Rco.toList.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Rco α) : List α
Std.Rco.toList.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rco α) : List α

Returns the elements of the given left-closed right-open range as a list in ascending order.

def

Std.Rco.size.{u} {α : Type u} [Std.Rxo.HasSize α] (r : Std.Rco α) : Nat
Std.Rco.size.{u} {α : Type u}
  [Std.Rxo.HasSize α] (r : Std.Rco α) :
  Nat

Returns the number of elements contained in the given left-closed right-open range.

def

Std.Rco.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Rco α) : Bool
Std.Rco.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Rco α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

structure

Std.Rcc.{u} (α : Type u) : Type u
Std.Rcc.{u} (α : Type u) : Type u

A range of elements of α with closed lower and upper bounds.

a...=b is the range of all values greater than or equal to a : α and less than or equal to b : α. This is notation for Rcc.mk a b.

Constructor

Std.Rcc.mk.{u}

Fields

lower : α

The lower bound of the range. lower is included in the range.

upper : α

The upper bound of the range. upper is included in the range.

def

Std.Rcc.iter.{u_1} {α : Type u_1} (r : Std.Rcc α) : Std.Iter α
Std.Rcc.iter.{u_1} {α : Type u_1}
  (r : Std.Rcc α) : Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Rcc.toArray.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Rcc α) : Array α
Std.Rcc.toArray.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Rcc α) : Array α

Returns the elements of the given closed range as an array in ascending order.

def

Std.Rcc.toList.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Rcc α) : List α
Std.Rcc.toList.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Rcc α) : List α

Returns the elements of the given closed range as a list in ascending order.

def

Std.Rcc.size.{u} {α : Type u} [Std.Rxc.HasSize α] (r : Std.Rcc α) : Nat
Std.Rcc.size.{u} {α : Type u}
  [Std.Rxc.HasSize α] (r : Std.Rcc α) :
  Nat

Returns the number of elements contained in the given closed range.

def

Std.Rcc.isEmpty.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Rcc α) : Bool
Std.Rcc.isEmpty.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Rcc α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLE instances.

structure

Std.Rci.{u} (α : Type u) : Type u
Std.Rci.{u} (α : Type u) : Type u

An upward-unbounded range of elements of α with a closed lower bound.

a...* is the range of all values greater than or equal to a : α. This is notation for Rci.mk a.

Constructor

Std.Rci.mk.{u}

Fields

lower : α

The lower bound of the range. lower is included in the range.

def

Std.Rci.iter.{u_1} {α : Type u_1} (r : Std.Rci α) : Std.Iter α
Std.Rci.iter.{u_1} {α : Type u_1}
  (r : Std.Rci α) : Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Rci.toArray.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : Array α
Std.Rci.toArray.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : Array α

Returns the elements of the given left-closed right-unbounded range as an array in ascending order.

def

Std.Rci.toList.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : List α
Std.Rci.toList.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : List α

Returns the elements of the given left-closed right-unbounded range as a list in ascending order.

def

Std.Rci.size.{u} {α : Type u} [Std.Rxi.HasSize α] (r : Std.Rci α) : Nat
Std.Rci.size.{u} {α : Type u}
  [Std.Rxi.HasSize α] (r : Std.Rci α) :
  Nat

Returns the number of elements contained in the given left-closed right-unbounded range.

def

Std.Rci.isEmpty.{u} {α : Type u} [Std.PRange.UpwardEnumerable α] :
  Std.Rci α → Bool
Std.Rci.isEmpty.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] :
  Std.Rci α → Bool

Checks whether the range contains any value. This function exists for completeness and always returns false: The closed lower bound is contained in the range, so left-closed right-unbounded ranges are never empty.

structure

Std.Roo.{u} (α : Type u) : Type u
Std.Roo.{u} (α : Type u) : Type u

A range of elements of α with an open lower and upper bounds.

a<...b or a<...<b is the range of all values greater than a : α and less than b : α. This is notation for Roo.mk a b.

Constructor

Std.Roo.mk.{u}

Fields

lower : α

The lower bound of the range. lower is not included in the range.

upper : α

The upper bound of the range. upper is not included in the range.

def

Std.Roo.iter.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Std.Iter α
Std.Roo.iter.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Roo.toArray.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Roo α) : Array α
Std.Roo.toArray.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Roo α) : Array α

Returns the elements of the given open range as an array in ascending order.

def

Std.Roo.toList.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Roo α) : List α
Std.Roo.toList.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Roo α) : List α

Returns the elements of the given open range as a list in ascending order.

def

Std.Roo.size.{u} {α : Type u} [Std.Rxo.HasSize α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roo α) : Nat
Std.Roo.size.{u} {α : Type u}
  [Std.Rxo.HasSize α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Nat

Returns the number of elements contained in the given open range.

def

Std.Roo.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roo α) : Bool
Std.Roo.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

structure

Std.Roc.{u} (α : Type u) : Type u
Std.Roc.{u} (α : Type u) : Type u

A range of elements of α with an open lower bound and a closed upper bound.

a<...=b is the range of all values greater than a : α and less than or equal to b : α. This is notation for Roc.mk a b.

Constructor

Std.Roc.mk.{u}

Fields

lower : α

The lower bound of the range. lower is not included in the range.

upper : α

The upper bound of the range. upper is included in the range.

def

Std.Roc.iter.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Std.Iter α
Std.Roc.iter.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Roc.toArray.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Roc α) : Array α
Std.Roc.toArray.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Roc α) : Array α

Returns the elements of the given left-open right-closed range as an array in ascending order.

def

Std.Roc.toList.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Roc α) : List α
Std.Roc.toList.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Roc α) : List α

Returns the elements of the given left-open right-closed range as a list in ascending order.

def

Std.Roc.size.{u} {α : Type u} [Std.Rxc.HasSize α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roc α) : Nat
Std.Roc.size.{u} {α : Type u}
  [Std.Rxc.HasSize α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Nat

Returns the number of elements contained in the given left-open right-closed range.

def

Std.Roc.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roc α) : Bool
Std.Roc.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

structure

Std.Roi.{u} (α : Type u) : Type u
Std.Roi.{u} (α : Type u) : Type u

An upward-unbounded range of elements of α with an open lower bound.

a<...* is the range of all values greater than a : α. This is notation for Roi.mk a.

Constructor

Std.Roi.mk.{u}

Fields

lower : α

The lower bound of the range. lower is not included in the range.

def

Std.Roi.iter.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Std.Iter α
Std.Roi.iter.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Roi.toArray.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : Array α
Std.Roi.toArray.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : Array α

Returns the elements of the given left-open right-unbounded range as an array in ascending order.

def

Std.Roi.toList.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : List α
Std.Roi.toList.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : List α

Returns the elements of the given left-open right-unbounded range as a list in ascending order.

def

Std.Roi.size.{u} {α : Type u} [Std.Rxi.HasSize α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roi α) : Nat
Std.Roi.size.{u} {α : Type u}
  [Std.Rxi.HasSize α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Nat

Returns the number of elements contained in the given left-open right-unbounded range.

def

Std.Roi.isEmpty.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Bool
Std.Roi.isEmpty.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Bool

Checks whether the range contains any value.

This function returns a meaningful value given a LawfulUpwardEnumerable instance.

structure

Std.Rio.{u} (α : Type u) : Type u
Std.Rio.{u} (α : Type u) : Type u

A downward-unbounded range of elements of α with an open upper bound.

*...b or *...<b is the range of all values less than b : α. This is notation for Rio.mk b.

Constructor

Std.Rio.mk.{u}

Fields

upper : α

The upper bound of the range. upper is not included in the range.

def

Std.Rio.iter.{u_1} {α : Type u_1} [Std.PRange.Least? α]
  (r : Std.Rio α) : Std.Iter α
Std.Rio.iter.{u_1} {α : Type u_1}
  [Std.PRange.Least? α] (r : Std.Rio α) :
  Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Rio.toArray.{u} {α : Type u} [Std.PRange.Least? α] [LT α]
  [DecidableLT α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : Array α
Std.Rio.toArray.{u} {α : Type u}
  [Std.PRange.Least? α] [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : Array α

Returns the elements of the given closed range as an array in ascending order.

def

Std.Rio.toList.{u} {α : Type u} [Std.PRange.Least? α] [LT α]
  [DecidableLT α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : List α
Std.Rio.toList.{u} {α : Type u}
  [Std.PRange.Least? α] [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : List α

Returns the elements of the given closed range as a list in ascending order.

def

Std.Rio.size.{u} {α : Type u} [Std.Rxo.HasSize α] [Std.PRange.Least? α]
  (r : Std.Rio α) : Nat
Std.Rio.size.{u} {α : Type u}
  [Std.Rxo.HasSize α]
  [Std.PRange.Least? α] (r : Std.Rio α) :
  Nat

Returns the number of elements contained in the given closed range.

def

Std.Rio.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.Least? α]
  (r : Std.Rio α) : Bool
Std.Rio.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rio α) :
  Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable, LawfulUpwardEnumerableLT and LawfulUpwardEnumerableLeast? instances.

structure

Std.Ric.{u} (α : Type u) : Type u
Std.Ric.{u} (α : Type u) : Type u

A downward-unbounded range of elements of α with a closed upper bound.

*...=b is the range of all values less than or equal to b : α. This is notation for Ric.mk b.

Constructor

Std.Ric.mk.{u}

Fields

upper : α

The upper bound of the range. upper is included in the range.

def

Std.Ric.iter.{u_1} {α : Type u_1} [Std.PRange.Least? α]
  (r : Std.Ric α) : Std.Iter α
Std.Ric.iter.{u_1} {α : Type u_1}
  [Std.PRange.Least? α] (r : Std.Ric α) :
  Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Ric.toArray.{u} {α : Type u} [Std.PRange.Least? α] [LE α]
  [DecidableLE α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : Array α
Std.Ric.toArray.{u} {α : Type u}
  [Std.PRange.Least? α] [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : Array α

Returns the elements of the given closed range as an array in ascending order.

def

Std.Ric.toList.{u} {α : Type u} [Std.PRange.Least? α] [LE α]
  [DecidableLE α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : List α
Std.Ric.toList.{u} {α : Type u}
  [Std.PRange.Least? α] [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : List α

Returns the elements of the given closed range as a list in ascending order.

def

Std.Ric.size.{u} {α : Type u} [Std.Rxc.HasSize α] [Std.PRange.Least? α]
  (r : Std.Ric α) : Nat
Std.Ric.size.{u} {α : Type u}
  [Std.Rxc.HasSize α]
  [Std.PRange.Least? α] (r : Std.Ric α) :
  Nat

Returns the number of elements contained in the given closed range.

def

Std.Ric.isEmpty.{u} {α : Type u} [Std.PRange.UpwardEnumerable α] :
  Std.Ric α → Bool
Std.Ric.isEmpty.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] :
  Std.Ric α → Bool

Checks whether the range contains any value. This function exists for completeness and always returns false: The closed upper bound is contained in the range, so left-unbounded right-closed ranges are never empty.

structure

Std.Rii.{u} (α : Type u) : Type
Std.Rii.{u} (α : Type u) : Type

A full range of all elements of α. Its only inhabitant is the range *...*, which is notation for Rii.mk.

Constructor

Std.Rii.mk.{u}

def

Std.Rii.iter.{u_1} {α : Type u_1} [Std.PRange.Least? α] :
  Std.Rii α → Std.Iter α
Std.Rii.iter.{u_1} {α : Type u_1}
  [Std.PRange.Least? α] :
  Std.Rii α → Std.Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

def

Std.Rii.toArray.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] : Array α
Std.Rii.toArray.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite
      (Std.Rxi.Iterator α) Id] :
  Array α

Returns the elements of the given full range as an array in ascending order.

def

Std.Rii.toList.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] : List α
Std.Rii.toList.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite
      (Std.Rxi.Iterator α) Id] :
  List α

Returns the elements of the given full range as a list in ascending order.

def

Std.Rii.size.{u} {α : Type u} :
  Std.Rii α → [Std.PRange.Least? α] → [Std.Rxi.HasSize α] → Nat
Std.Rii.size.{u} {α : Type u} :
  Std.Rii α →
    [Std.PRange.Least? α] →
      [Std.Rxi.HasSize α] → Nat

Returns the number of elements contained in the full range.

def

Std.Rii.isEmpty.{u} {α : Type u} [Std.PRange.Least? α] :
  Std.Rii α → Bool
Std.Rii.isEmpty.{u} {α : Type u}
  [Std.PRange.Least? α] : Std.Rii α → Bool

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLeast? instances.

20.18.2. 范围相关的 Type 类🔗

type class

Std.PRange.UpwardEnumerable.{u} (α : Type u) : Type u
Std.PRange.UpwardEnumerable.{u}
  (α : Type u) : Type u

This typeclass provides the function succ? : α → Option α that computes the successor of elements of α, or none if no successor exists. It also provides the function succMany?, which computes n-th successors.

succ? is expected to be acyclic: No element is its own transitive successor. If α is ordered, then every element larger than a : α should be a transitive successor of a. These properties and the compatibility of succ? with succMany? are encoded in the typeclasses LawfulUpwardEnumerable, LawfulUpwardEnumerableLE and LawfulUpwardEnumerableLT.

Instance Constructor

Std.PRange.UpwardEnumerable.mk.{u}

Methods

succ? : α → Option α

Maps elements of α to their successor, or none if no successor exists.

succMany? : Nat → α → Option α

Maps elements of α to their n-th successor, or none if no successor exists. This should semantically behave like repeatedly applying succ?, but it might be more efficient.

LawfulUpwardEnumerable ensures the compatibility with succ?.

If no other implementation is provided in UpwardEnumerable instance, succMany? repeatedly applies succ?.

def

Std.PRange.UpwardEnumerable.LE.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] (a b : α) : Prop
Std.PRange.UpwardEnumerable.LE.{u}
  {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  (a b : α) : Prop

According to UpwardEnumerable.LE, a is less than or equal to b if b is a or a transitive successor of a.

def

Std.PRange.UpwardEnumerable.LT.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] (a b : α) : Prop
Std.PRange.UpwardEnumerable.LT.{u}
  {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  (a b : α) : Prop

According to UpwardEnumerable.LT, a is less than b if b is a proper transitive successor of a. 'Proper' means that b is the n-th successor of a, where n > 0.

Given LawfulUpwardEnumerable α, no element of α is less than itself.

type class

Std.PRange.LawfulUpwardEnumerable.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.PRange.LawfulUpwardEnumerable.{u}
  (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

This typeclass ensures that an UpwardEnumerable α instance is well-behaved.

Instance Constructor

Std.PRange.LawfulUpwardEnumerable.mk.{u}

Methods

ne_of_lt : ∀ (a b : α), Std.PRange.UpwardEnumerable.LT a b → a ≠ b

There is no cyclic chain of successors.

succMany?_zero : ∀ (a : α), Std.PRange.succMany? 0 a = some a

The 0-th successor of a is a itself.

succMany?_add_one : ∀ (n : Nat) (a : α), Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?

The n + 1-th successor of a is the successor of the n-th successor, given that said successors actually exist.

type class

Std.PRange.Least?.{u} (α : Type u) : Type u
Std.PRange.Least?.{u} (α : Type u) :
  Type u

The typeclass Least? α optionally provides a smallest element of α, least? : Option α.

The main use case of this typeclass is to use it in combination with UpwardEnumerable to obtain a (possibly infinite) ascending enumeration of all elements of α.

Instance Constructor

Std.PRange.Least?.mk.{u}

Methods

least? : Option α

Returns the smallest element of α, or none if α is empty.

Only empty types are allowed to define least? := none. If α is ordered and nonempty, then the value of least? should be the smallest element according to the order on α.

type class

Std.PRange.InfinitelyUpwardEnumerable.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.PRange.InfinitelyUpwardEnumerable.{u}
  (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

This propositional typeclass ensures that UpwardEnumerable.succ? will never return none. In other words, it ensures that there will always be a successor.

Instance Constructor

Std.PRange.InfinitelyUpwardEnumerable.mk.{u}

Methods

isSome_succ? : ∀ (a : α), (Std.PRange.succ? a).isSome = true

Every element of α has a successor.

type class

Std.PRange.LinearlyUpwardEnumerable.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.PRange.LinearlyUpwardEnumerable.{u}
  (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

This propositional typeclass ensures that UpwardEnumerable.succ? is injective.

Instance Constructor

Std.PRange.LinearlyUpwardEnumerable.mk.{u}

Methods

eq_of_succ?_eq : ∀ (a b : α), Std.PRange.succ? a = Std.PRange.succ? b → a = b

The implementation of UpwardEnumerable.succ? for α is injective.

type class

Std.Rxi.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.Rxi.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

This type class ensures that right-unbounded ranges (i.e., for a bound a, a...*, a<...* and *...*) are always finite. This is a prerequisite for many functions and instances, such as Rci.toList or ForIn'.

Instance Constructor

Std.Rxi.IsAlwaysFinite.mk.{u}

Methods

finite : ∀ (init : α), ∃ n, Std.PRange.succMany? n init = none

For every elements init, there exists a chain of successors that results in an element that has no successors.

type class

Std.Rxi.HasSize.{u} (α : Type u) : Type u
Std.Rxi.HasSize.{u} (α : Type u) : Type u

This typeclass provides support for the size function for ranges with closed lower bound (Ric.size, Rio.size and Rii.size).

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulHasSize.

Instance Constructor

Std.Rxi.HasSize.mk.{u}

Methods

size : α → Nat

Returns the number of elements starting from lo that satisfy the given upper bound.

type class

Std.Rxc.IsAlwaysFinite.{u} (α : Type u) [Std.PRange.UpwardEnumerable α]
  [LE α] : Prop
Std.Rxc.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] [LE α] :
  Prop

This type class ensures that right-closed ranges (i.e., for bounds a and b, a...=b, a<...=b and *...=b) are always finite. This is a prerequisite for many functions and instances, such as Rcc.toList or ForIn'.

Instance Constructor

Std.Rxc.IsAlwaysFinite.mk.{u}

Methods

finite : ∀ (init hi : α), ∃ n, (Std.PRange.succMany? n init).elim True fun x => ¬x ≤ hi

For every pair of elements init and hi, there exists a chain of successors that results in an element that either has no successors or is greater than hi.

type class

Std.Rxc.HasSize.{u} (α : Type u) : Type u
Std.Rxc.HasSize.{u} (α : Type u) : Type u

This typeclass provides support for the size function for ranges with closed lower bound (Rcc.size, Rco.size and Rci.size).

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulHasSize.

Instance Constructor

Std.Rxc.HasSize.mk.{u}

Methods

size : α → α → Nat

Returns the number of elements starting from lo that satisfy the given upper bound.

20.18.3. 实施范围🔗

内置范围类型可以与任何类型一起使用，但它们的有用性取决于某些类型类实例的存在。一般来说，范围要么检查成员资格，要么枚举或迭代。要检查某个值是否包含在某个范围内，请使用 DecidableLT 和 DecidableLE 实例将该值与该范围各自的开端点和闭端点进行比较。要获取范围的迭代器，只需要 Std.PRange.UpwardEnumerable 和 Std.PRange.LawfulUpwardEnumerable 的实例。要在 Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for 循环中直接迭代它，还需要 Std.PRange.LawfulUpwardEnumerableLE 和 Std.PRange.LawfulUpwardEnumerableLT。要枚举一个范围（例如通过调用 toList），必须证明它是有限的。这是通过提供 Std.Rxi.IsAlwaysFinite、Std.Rxc.IsAlwaysFinite 或 Std.Rxo.IsAlwaysFinite 的实例来完成的。

Implementing Ranges

枚举类型 Day 表示星期几：

inductive Day where
  | mo | tu | we | th | fr | sa | su
deriving Repr

虽然已经可以在范围内使用这种类型，但它们并不是特别有用。没有会员实例：

#eval failed to synthesize instance of type class
  Membership Day (Std.Rcc Day)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.Day.we ∈ (Day.mo...=Day.fr)

failed to synthesize instance of type class
  Membership Day (Std.Rcc Day)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

范围不能迭代：

#eval show IO Unit from
  failed to synthesize instance for 'for_in%' notation
  ForIn (EIO IO.Error) (Std.Rcc Day) ?m.11for d in Day.mo...=Day.fr do
    IO.println s!"It's {repr d}"

failed to synthesize instance for 'for_in%' notation
  ForIn (EIO IO.Error) (Std.Rcc Day) ?m.11

即使类型是有限的，它们也不能被枚举：

#eval failed to synthesize instance of type class
  Std.PRange.UpwardEnumerable Day

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.(Day.sa...*).toList

failed to synthesize instance of type class
  Std.PRange.UpwardEnumerable Day

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

成员资格测试需要 DecidableLT 和 DecidableLE 实例。获得这些的一个简单方法是每天进行编号，并比较这些数字：

def Day.toNat : Day → Nat
  | mo => 0
  | tu => 1
  | we => 2
  | th => 3
  | fr => 4
  | sa => 5
  | su => 6

instance : LT Day where
  lt d1 d2 := d1.toNat < d2.toNat

instance : LE Day where
  le d1 d2 := d1.toNat ≤ d2.toNat

instance : DecidableLT Day :=
  fun d1 d2 => inferInstanceAs (Decidable (d1.toNat < d2.toNat))

instance : DecidableLE Day :=
  fun d1 d2 => inferInstanceAs (Decidable (d1.toNat ≤ d2.toNat))

有了这些可用实例，成员资格测试就可以按预期进行：

def Day.isWeekday (d : Day) : Bool := d ∈ Day.mo...Day.sa

true#eval Day.th.isWeekday

true

false#eval Day.sa.isWeekday

false

迭代和枚举都是重复应用后继函数的变体，直到达到范围的上限或类型的最大元素。该后继函数是 Std.PRange.UpwardEnumerable.succ?。在 Day 的命名空间中定义函数以与通用字段表示法一起使用也很方便：

def Day.succ? : Day → Option Day
  | mo => some tu
  | tu => some we
  | we => some th
  | th => some fr
  | fr => some sa
  | sa => some su
  | su => none

instance : Std.PRange.UpwardEnumerable Day where
  succ? := Day.succ?

迭代还需要证明 succ? 的实现是合理的。其属性以 Std.PRange.UpwardEnumerable.succMany? 表示，它迭代 succ? 的应用一定次数，并具有以 Nat.repeat 和 succ? 形式的默认实现。特别是，LawfulUpwardEnumerable 的实例需要证明 Std.PRange.UpwardEnumerable.succMany? 对应于默认实现，以及重复应用后继永远不会再次产生相同元素的证明。

第一步是为关于 succMany? 的两个证明编写两个辅助引理。虽然它们可以内联写入实例声明中，但它们具有 @[simp] 属性很方便。

@[simp]
theorem Day.succMany?_zero (d : Day) :
  Std.PRange.succMany? 0 d = some d := byd:Day⊢ Std.PRange.succMany? 0 d = some d
  simp [Std.PRange.succMany?, Nat.repeat]All goals completed! 🐙

@[simp]
theorem Day.succMany?_add_one (n : Nat) (d : Day) :
    Std.PRange.succMany? (n + 1) d =
    (Std.PRange.succMany? n d).bind Std.PRange.succ? := byn:Natd:Day⊢ Std.PRange.succMany? (n + 1) d = (Std.PRange.succMany? n d).bind Std.PRange.succ?
  simp [Std.PRange.succMany?, Nat.repeat, Std.PRange.succ?]All goals completed! 🐙

证明后继中没有循环使用一个方便的辅助引理来计算任意两天之间的后继步骤数。它被标记为 @[grind →] ，因为当存在与其前提相匹配的假设时，它会添加大量新信息：

@[grind →]
theorem Day.succMany?_steps {d d' : Day} {steps} :
    Std.PRange.succMany? steps d = some d' →
    if d ≤ d' then steps = d'.toNat - d.toNat
    else False := byd:Dayd':Daysteps:Nat⊢ Std.PRange.succMany? steps d = some d' → if d ≤ d' then steps = d'.toNat - d.toNat else False
  intro hd:Dayd':Daysteps:Nath:Std.PRange.succMany? steps d = some d'⊢ if d ≤ d' then steps = d'.toNat - d.toNat else False
  match steps with
  | 0 | 1 | 2 | 3 | 4 | 5 | 6 =>d:Dayd':Daysteps:Nath:Std.PRange.succMany? 6 d = some d'⊢ if d ≤ d' then 6 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 5 d = some d'⊢ if d ≤ d' then 5 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 4 d = some d'⊢ if d ≤ d' then 4 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 3 d = some d'⊢ if d ≤ d' then 3 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 2 d = some d'⊢ if d ≤ d' then 2 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 1 d = some d'⊢ if d ≤ d' then 1 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 0 d = some d'⊢ if d ≤ d' then 0 = d'.toNat - d.toNat else False
    cases dmod':Daysteps:Nath:Std.PRange.succMany? 6 mo = some d'⊢ if mo ≤ d' then 6 = d'.toNat - mo.toNat else Falsetud':Daysteps:Nath:Std.PRange.succMany? 6 tu = some d'⊢ if tu ≤ d' then 6 = d'.toNat - tu.toNat else Falsewed':Daysteps:Nath:Std.PRange.succMany? 6 we = some d'⊢ if we ≤ d' then 6 = d'.toNat - we.toNat else Falsethd':Daysteps:Nath:Std.PRange.succMany? 6 th = some d'⊢ if th ≤ d' then 6 = d'.toNat - th.toNat else Falsefrd':Daysteps:Nath:Std.PRange.succMany? 6 fr = some d'⊢ if fr ≤ d' then 6 = d'.toNat - fr.toNat else Falsesad':Daysteps:Nath:Std.PRange.succMany? 6 sa = some d'⊢ if sa ≤ d' then 6 = d'.toNat - sa.toNat else Falsesud':Daysteps:Nath:Std.PRange.succMany? 6 su = some d'⊢ if su ≤ d' then 6 = d'.toNat - su.toNat else False <;>mod':Daysteps:Nath:Std.PRange.succMany? 6 mo = some d'⊢ if mo ≤ d' then 6 = d'.toNat - mo.toNat else Falsetud':Daysteps:Nath:Std.PRange.succMany? 6 tu = some d'⊢ if tu ≤ d' then 6 = d'.toNat - tu.toNat else Falsewed':Daysteps:Nath:Std.PRange.succMany? 6 we = some d'⊢ if we ≤ d' then 6 = d'.toNat - we.toNat else Falsethd':Daysteps:Nath:Std.PRange.succMany? 6 th = some d'⊢ if th ≤ d' then 6 = d'.toNat - th.toNat else Falsefrd':Daysteps:Nath:Std.PRange.succMany? 6 fr = some d'⊢ if fr ≤ d' then 6 = d'.toNat - fr.toNat else Falsesad':Daysteps:Nath:Std.PRange.succMany? 6 sa = some d'⊢ if sa ≤ d' then 6 = d'.toNat - sa.toNat else Falsesud':Daysteps:Nath:Std.PRange.succMany? 6 su = some d'⊢ if su ≤ d' then 6 = d'.toNat - su.toNat else False cases d'su.mosteps:Nath:Std.PRange.succMany? 6 su = some mo⊢ if su ≤ mo then 6 = mo.toNat - su.toNat else Falsesu.tusteps:Nath:Std.PRange.succMany? 6 su = some tu⊢ if su ≤ tu then 6 = tu.toNat - su.toNat else Falsesu.westeps:Nath:Std.PRange.succMany? 6 su = some we⊢ if su ≤ we then 6 = we.toNat - su.toNat else Falsesu.thsteps:Nath:Std.PRange.succMany? 6 su = some th⊢ if su ≤ th then 6 = th.toNat - su.toNat else Falsesu.frsteps:Nath:Std.PRange.succMany? 6 su = some fr⊢ if su ≤ fr then 6 = fr.toNat - su.toNat else Falsesu.sasteps:Nath:Std.PRange.succMany? 6 su = some sa⊢ if su ≤ sa then 6 = sa.toNat - su.toNat else Falsesu.susteps:Nath:Std.PRange.succMany? 6 su = some su⊢ if su ≤ su then 6 = su.toNat - su.toNat else False <;>mo.mosteps:Nath:Std.PRange.succMany? 6 mo = some mo⊢ if mo ≤ mo then 6 = mo.toNat - mo.toNat else Falsemo.tusteps:Nath:Std.PRange.succMany? 6 mo = some tu⊢ if mo ≤ tu then 6 = tu.toNat - mo.toNat else Falsemo.westeps:Nath:Std.PRange.succMany? 6 mo = some we⊢ if mo ≤ we then 6 = we.toNat - mo.toNat else Falsemo.thsteps:Nath:Std.PRange.succMany? 6 mo = some th⊢ if mo ≤ th then 6 = th.toNat - mo.toNat else Falsemo.frsteps:Nath:Std.PRange.succMany? 6 mo = some fr⊢ if mo ≤ fr then 6 = fr.toNat - mo.toNat else Falsemo.sasteps:Nath:Std.PRange.succMany? 6 mo = some sa⊢ if mo ≤ sa then 6 = sa.toNat - mo.toNat else Falsemo.susteps:Nath:Std.PRange.succMany? 6 mo = some su⊢ if mo ≤ su then 6 = su.toNat - mo.toNat else Falsetu.mosteps:Nath:Std.PRange.succMany? 6 tu = some mo⊢ if tu ≤ mo then 6 = mo.toNat - tu.toNat else Falsetu.tusteps:Nath:Std.PRange.succMany? 6 tu = some tu⊢ if tu ≤ tu then 6 = tu.toNat - tu.toNat else Falsetu.westeps:Nath:Std.PRange.succMany? 6 tu = some we⊢ if tu ≤ we then 6 = we.toNat - tu.toNat else Falsetu.thsteps:Nath:Std.PRange.succMany? 6 tu = some th⊢ if tu ≤ th then 6 = th.toNat - tu.toNat else Falsetu.frsteps:Nath:Std.PRange.succMany? 6 tu = some fr⊢ if tu ≤ fr then 6 = fr.toNat - tu.toNat else Falsetu.sasteps:Nath:Std.PRange.succMany? 6 tu = some sa⊢ if tu ≤ sa then 6 = sa.toNat - tu.toNat else Falsetu.susteps:Nath:Std.PRange.succMany? 6 tu = some su⊢ if tu ≤ su then 6 = su.toNat - tu.toNat else Falsewe.mosteps:Nath:Std.PRange.succMany? 6 we = some mo⊢ if we ≤ mo then 6 = mo.toNat - we.toNat else Falsewe.tusteps:Nath:Std.PRange.succMany? 6 we = some tu⊢ if we ≤ tu then 6 = tu.toNat - we.toNat else Falsewe.westeps:Nath:Std.PRange.succMany? 6 we = some we⊢ if we ≤ we then 6 = we.toNat - we.toNat else Falsewe.thsteps:Nath:Std.PRange.succMany? 6 we = some th⊢ if we ≤ th then 6 = th.toNat - we.toNat else Falsewe.frsteps:Nath:Std.PRange.succMany? 6 we = some fr⊢ if we ≤ fr then 6 = fr.toNat - we.toNat else Falsewe.sasteps:Nath:Std.PRange.succMany? 6 we = some sa⊢ if we ≤ sa then 6 = sa.toNat - we.toNat else Falsewe.susteps:Nath:Std.PRange.succMany? 6 we = some su⊢ if we ≤ su then 6 = su.toNat - we.toNat else Falseth.mosteps:Nath:Std.PRange.succMany? 6 th = some mo⊢ if th ≤ mo then 6 = mo.toNat - th.toNat else Falseth.tusteps:Nath:Std.PRange.succMany? 6 th = some tu⊢ if th ≤ tu then 6 = tu.toNat - th.toNat else Falseth.westeps:Nath:Std.PRange.succMany? 6 th = some we⊢ if th ≤ we then 6 = we.toNat - th.toNat else Falseth.thsteps:Nath:Std.PRange.succMany? 6 th = some th⊢ if th ≤ th then 6 = th.toNat - th.toNat else Falseth.frsteps:Nath:Std.PRange.succMany? 6 th = some fr⊢ if th ≤ fr then 6 = fr.toNat - th.toNat else Falseth.sasteps:Nath:Std.PRange.succMany? 6 th = some sa⊢ if th ≤ sa then 6 = sa.toNat - th.toNat else Falseth.susteps:Nath:Std.PRange.succMany? 6 th = some su⊢ if th ≤ su then 6 = su.toNat - th.toNat else Falsefr.mosteps:Nath:Std.PRange.succMany? 6 fr = some mo⊢ if fr ≤ mo then 6 = mo.toNat - fr.toNat else Falsefr.tusteps:Nath:Std.PRange.succMany? 6 fr = some tu⊢ if fr ≤ tu then 6 = tu.toNat - fr.toNat else Falsefr.westeps:Nath:Std.PRange.succMany? 6 fr = some we⊢ if fr ≤ we then 6 = we.toNat - fr.toNat else Falsefr.thsteps:Nath:Std.PRange.succMany? 6 fr = some th⊢ if fr ≤ th then 6 = th.toNat - fr.toNat else Falsefr.frsteps:Nath:Std.PRange.succMany? 6 fr = some fr⊢ if fr ≤ fr then 6 = fr.toNat - fr.toNat else Falsefr.sasteps:Nath:Std.PRange.succMany? 6 fr = some sa⊢ if fr ≤ sa then 6 = sa.toNat - fr.toNat else Falsefr.susteps:Nath:Std.PRange.succMany? 6 fr = some su⊢ if fr ≤ su then 6 = su.toNat - fr.toNat else Falsesa.mosteps:Nath:Std.PRange.succMany? 6 sa = some mo⊢ if sa ≤ mo then 6 = mo.toNat - sa.toNat else Falsesa.tusteps:Nath:Std.PRange.succMany? 6 sa = some tu⊢ if sa ≤ tu then 6 = tu.toNat - sa.toNat else Falsesa.westeps:Nath:Std.PRange.succMany? 6 sa = some we⊢ if sa ≤ we then 6 = we.toNat - sa.toNat else Falsesa.thsteps:Nath:Std.PRange.succMany? 6 sa = some th⊢ if sa ≤ th then 6 = th.toNat - sa.toNat else Falsesa.frsteps:Nath:Std.PRange.succMany? 6 sa = some fr⊢ if sa ≤ fr then 6 = fr.toNat - sa.toNat else Falsesa.sasteps:Nath:Std.PRange.succMany? 6 sa = some sa⊢ if sa ≤ sa then 6 = sa.toNat - sa.toNat else Falsesa.susteps:Nath:Std.PRange.succMany? 6 sa = some su⊢ if sa ≤ su then 6 = su.toNat - sa.toNat else Falsesu.mosteps:Nath:Std.PRange.succMany? 6 su = some mo⊢ if su ≤ mo then 6 = mo.toNat - su.toNat else Falsesu.tusteps:Nath:Std.PRange.succMany? 6 su = some tu⊢ if su ≤ tu then 6 = tu.toNat - su.toNat else Falsesu.westeps:Nath:Std.PRange.succMany? 6 su = some we⊢ if su ≤ we then 6 = we.toNat - su.toNat else Falsesu.thsteps:Nath:Std.PRange.succMany? 6 su = some th⊢ if su ≤ th then 6 = th.toNat - su.toNat else Falsesu.frsteps:Nath:Std.PRange.succMany? 6 su = some fr⊢ if su ≤ fr then 6 = fr.toNat - su.toNat else Falsesu.sasteps:Nath:Std.PRange.succMany? 6 su = some sa⊢ if su ≤ sa then 6 = sa.toNat - su.toNat else Falsesu.susteps:Nath:Std.PRange.succMany? 6 su = some su⊢ if su ≤ su then 6 = su.toNat - su.toNat else False
    simp_all +decide [Std.PRange.succMany?, Nat.repeat, Day.succ?]All goals completed! 🐙
  | n + 7 =>d:Dayd':Daysteps:Natn:Nath:Std.PRange.succMany? (n + 7) d = some d'⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
    simp at hd:Dayd':Daysteps:Natn:Nath:(((((((Std.PRange.succMany? n d).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
                Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
    cases h' : (Std.PRange.succMany? n d) with
    | none =>noned:Dayd':Daysteps:Natn:Nath:(((((((Std.PRange.succMany? n d).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
                Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = none⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
      simp_allAll goals completed! 🐙
    | some d'' =>somed:Dayd':Daysteps:Natn:Nath:(((((((Std.PRange.succMany? n d).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
                Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'd'':Dayh':Std.PRange.succMany? n d = some d''⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
      rw [h'somed:Dayd':Daysteps:Natn:Natd'':Dayh:(((((((some d'').bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some d''⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False] at hsomed:Dayd':Daysteps:Natn:Natd'':Dayh:(((((((some d'').bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some d''⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
      cases d''some.mod:Dayd':Daysteps:Natn:Nath:(((((((some mo).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some mo⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.tud:Dayd':Daysteps:Natn:Nath:(((((((some tu).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some tu⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.wed:Dayd':Daysteps:Natn:Nath:(((((((some we).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some we⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.thd:Dayd':Daysteps:Natn:Nath:(((((((some th).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some th⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.frd:Dayd':Daysteps:Natn:Nath:(((((((some fr).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some fr⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sad:Dayd':Daysteps:Natn:Nath:(((((((some sa).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some sa⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sud:Dayd':Daysteps:Natn:Nath:(((((((some su).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some su⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False <;>some.mod:Dayd':Daysteps:Natn:Nath:(((((((some mo).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some mo⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.tud:Dayd':Daysteps:Natn:Nath:(((((((some tu).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some tu⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.wed:Dayd':Daysteps:Natn:Nath:(((((((some we).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some we⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.thd:Dayd':Daysteps:Natn:Nath:(((((((some th).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some th⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.frd:Dayd':Daysteps:Natn:Nath:(((((((some fr).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some fr⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sad:Dayd':Daysteps:Natn:Nath:(((((((some sa).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some sa⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sud:Dayd':Daysteps:Natn:Nath:(((((((some su).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some su⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False contradictionAll goals completed! 🐙

有了这个助手，证明就相当简短了：

instance : Std.PRange.LawfulUpwardEnumerable Day where
  ne_of_lt d1 d2 h := byd1:Dayd2:Dayh:Std.PRange.UpwardEnumerable.LT d1 d2⊢ d1 ≠ d2 grind [Std.PRange.UpwardEnumerable.LT]All goals completed! 🐙
  succMany?_zero := Day.succMany?_zero
  succMany?_add_one := Day.succMany?_add_one

证明三种可枚举范围是有限的使得枚举天数范围成为可能：

instance : Std.Rxo.IsAlwaysFinite Day where
  finite init hi :=
    ⟨7, byinit:Dayhi:Day⊢ (Std.PRange.succMany? 7 init).elim True fun x => ¬x < hi cases initmohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x < hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x < hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x < hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x < hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x < hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x < hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x < hi <;>mohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x < hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x < hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x < hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x < hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x < hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x < hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x < hi simp [Std.PRange.succ?, Day.succ?]All goals completed! 🐙⟩

instance : Std.Rxc.IsAlwaysFinite Day where
  finite init hi :=
    ⟨7, byinit:Dayhi:Day⊢ (Std.PRange.succMany? 7 init).elim True fun x => ¬x ≤ hi cases initmohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x ≤ hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x ≤ hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x ≤ hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x ≤ hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x ≤ hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x ≤ hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x ≤ hi <;>mohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x ≤ hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x ≤ hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x ≤ hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x ≤ hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x ≤ hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x ≤ hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x ≤ hi simp [Std.PRange.succ?, Day.succ?]All goals completed! 🐙⟩

instance : Std.Rxi.IsAlwaysFinite Day where
  finite init := ⟨7, byinit:Day⊢ Std.PRange.succMany? 7 init = none cases initmo⊢ Std.PRange.succMany? 7 Day.mo = nonetu⊢ Std.PRange.succMany? 7 Day.tu = nonewe⊢ Std.PRange.succMany? 7 Day.we = noneth⊢ Std.PRange.succMany? 7 Day.th = nonefr⊢ Std.PRange.succMany? 7 Day.fr = nonesa⊢ Std.PRange.succMany? 7 Day.sa = nonesu⊢ Std.PRange.succMany? 7 Day.su = none <;>mo⊢ Std.PRange.succMany? 7 Day.mo = nonetu⊢ Std.PRange.succMany? 7 Day.tu = nonewe⊢ Std.PRange.succMany? 7 Day.we = noneth⊢ Std.PRange.succMany? 7 Day.th = nonefr⊢ Std.PRange.succMany? 7 Day.fr = nonesa⊢ Std.PRange.succMany? 7 Day.sa = nonesu⊢ Std.PRange.succMany? 7 Day.su = none rflAll goals completed! 🐙⟩

def allWeekdays : List Day := (Day.mo...Day.sa).toList
[Day.mo, Day.tu, Day.we, Day.th, Day.fr]#eval allWeekdays

[Day.mo, Day.tu, Day.we, Day.th, Day.fr]

添加 Std.PRange.Least? 实例允许枚举左无界范围：

instance : Std.PRange.Least? Day where
  least? := some .mo

def allWeekdays' : List Day := (*...Day.sa).toList
[Day.mo, Day.tu, Day.we, Day.th, Day.fr]#eval allWeekdays'

[Day.mo, Day.tu, Day.we, Day.th, Day.fr]

还可以创建一个可枚举的迭代器，但它还不能与 Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for 一起使用：

[Day.we, Day.th]#eval (Day.we...Day.fr).iter.toList

[Day.we, Day.th]

#eval show IO Unit from do
  failed to synthesize instance for 'for_in%' notation
  ForIn (EIO IO.Error) (Std.Iter Day) ?m.12for d in (Day.mo...Day.th).iter do
    IO.println s!"It's {repr d}."

failed to synthesize instance for 'for_in%' notation
  ForIn (EIO IO.Error) (Std.Iter Day) ?m.12

启用迭代从而使天数范围功能齐全的最后一步是证明 Day 上的小于和小于或等于关系对应于通过迭代后继函数导出的不等式概念。这是在类 Std.PRange.LawfulUpwardEnumerableLT 和 Std.PRange.LawfulUpwardEnumerableLE 中捕获的，这要求这两个概念在逻辑上是等效的：

instance : Std.PRange.LawfulUpwardEnumerableLT Day where
  lt_iff d1 d2 := byd1:Dayd2:Day⊢ d1 < d2 ↔ Std.PRange.UpwardEnumerable.LT d1 d2
    constructormpd1:Dayd2:Day⊢ d1 < d2 → Std.PRange.UpwardEnumerable.LT d1 d2mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LT d1 d2 → d1 < d2
    .mpd1:Dayd2:Day⊢ d1 < d2 → Std.PRange.UpwardEnumerable.LT d1 d2 intro ltmpd1:Dayd2:Daylt:d1 < d2⊢ Std.PRange.UpwardEnumerable.LT d1 d2
      simp only [Std.PRange.UpwardEnumerable.LT, Day.succMany?_add_one]mpd1:Dayd2:Daylt:d1 < d2⊢ ∃ n, (Std.PRange.succMany? n d1).bind Std.PRange.succ? = some d2
      exists d2.toNat - d1.toNat.succmpd1:Dayd2:Daylt:d1 < d2⊢ (Std.PRange.succMany? (d2.toNat - d1.toNat.succ) d1).bind Std.PRange.succ? = some d2
      cases d1mp.mod2:Daylt:Day.mo < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some d2mp.tud2:Daylt:Day.tu < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some d2mp.wed2:Daylt:Day.we < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some d2mp.thd2:Daylt:Day.th < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some d2mp.frd2:Daylt:Day.fr < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some d2mp.sad2:Daylt:Day.sa < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some d2mp.sud2:Daylt:Day.su < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some d2 <;>mp.mod2:Daylt:Day.mo < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some d2mp.tud2:Daylt:Day.tu < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some d2mp.wed2:Daylt:Day.we < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some d2mp.thd2:Daylt:Day.th < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some d2mp.frd2:Daylt:Day.fr < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some d2mp.sad2:Daylt:Day.sa < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some d2mp.sud2:Daylt:Day.su < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some d2 cases d2mp.su.molt:Day.su < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.momp.su.tult:Day.su < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.tump.su.welt:Day.su < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.wemp.su.thlt:Day.su < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.thmp.su.frlt:Day.su < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.frmp.su.salt:Day.su < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.samp.su.sult:Day.su < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.su <;>mp.mo.molt:Day.mo < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.momp.mo.tult:Day.mo < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.tump.mo.welt:Day.mo < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.wemp.mo.thlt:Day.mo < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.thmp.mo.frlt:Day.mo < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.frmp.mo.salt:Day.mo < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.samp.mo.sult:Day.mo < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.sump.tu.molt:Day.tu < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.momp.tu.tult:Day.tu < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.tump.tu.welt:Day.tu < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.wemp.tu.thlt:Day.tu < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.thmp.tu.frlt:Day.tu < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.frmp.tu.salt:Day.tu < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.samp.tu.sult:Day.tu < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.sump.we.molt:Day.we < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.momp.we.tult:Day.we < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.tump.we.welt:Day.we < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.wemp.we.thlt:Day.we < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.thmp.we.frlt:Day.we < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.frmp.we.salt:Day.we < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.samp.we.sult:Day.we < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.sump.th.molt:Day.th < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.momp.th.tult:Day.th < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.tump.th.welt:Day.th < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.wemp.th.thlt:Day.th < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.thmp.th.frlt:Day.th < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.frmp.th.salt:Day.th < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.samp.th.sult:Day.th < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.sump.fr.molt:Day.fr < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.momp.fr.tult:Day.fr < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.tump.fr.welt:Day.fr < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.wemp.fr.thlt:Day.fr < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.thmp.fr.frlt:Day.fr < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.frmp.fr.salt:Day.fr < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.samp.fr.sult:Day.fr < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.sump.sa.molt:Day.sa < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.momp.sa.tult:Day.sa < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.tump.sa.welt:Day.sa < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.wemp.sa.thlt:Day.sa < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.thmp.sa.frlt:Day.sa < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.frmp.sa.salt:Day.sa < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.samp.sa.sult:Day.sa < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.sump.su.molt:Day.su < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.momp.su.tult:Day.su < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.tump.su.welt:Day.su < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.wemp.su.thlt:Day.su < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.thmp.su.frlt:Day.su < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.frmp.su.salt:Day.su < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.samp.su.sult:Day.su < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.su
      simp_all [Day.toNat, Std.PRange.succ?, Day.succ?]mp.su.sult:Day.su < Day.su⊢ False <;>mp.mo.molt:Day.mo < Day.mo⊢ Falsemp.tu.molt:Day.tu < Day.mo⊢ Falsemp.tu.tult:Day.tu < Day.tu⊢ Falsemp.we.molt:Day.we < Day.mo⊢ Falsemp.we.tult:Day.we < Day.tu⊢ Falsemp.we.welt:Day.we < Day.we⊢ Falsemp.th.molt:Day.th < Day.mo⊢ Falsemp.th.tult:Day.th < Day.tu⊢ Falsemp.th.welt:Day.th < Day.we⊢ Falsemp.th.thlt:Day.th < Day.th⊢ Falsemp.fr.molt:Day.fr < Day.mo⊢ Falsemp.fr.tult:Day.fr < Day.tu⊢ Falsemp.fr.welt:Day.fr < Day.we⊢ Falsemp.fr.thlt:Day.fr < Day.th⊢ Falsemp.fr.frlt:Day.fr < Day.fr⊢ Falsemp.sa.molt:Day.sa < Day.mo⊢ Falsemp.sa.tult:Day.sa < Day.tu⊢ Falsemp.sa.welt:Day.sa < Day.we⊢ Falsemp.sa.thlt:Day.sa < Day.th⊢ Falsemp.sa.frlt:Day.sa < Day.fr⊢ Falsemp.sa.salt:Day.sa < Day.sa⊢ Falsemp.su.molt:Day.su < Day.mo⊢ Falsemp.su.tult:Day.su < Day.tu⊢ Falsemp.su.welt:Day.su < Day.we⊢ Falsemp.su.thlt:Day.su < Day.th⊢ Falsemp.su.frlt:Day.su < Day.fr⊢ Falsemp.su.salt:Day.su < Day.sa⊢ Falsemp.su.sult:Day.su < Day.su⊢ False
      contradictionAll goals completed! 🐙
    .mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LT d1 d2 → d1 < d2 intro ⟨steps, eq⟩mprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) d1 = some d2⊢ d1 < d2
      have := Day.succMany?_steps eqmprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) d1 = some d2this:if d1 ≤ d2 then steps + 1 = d2.toNat - d1.toNat else False⊢ d1 < d2
      cases d1mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some d2this:if Day.mo ≤ d2 then steps + 1 = d2.toNat - Day.mo.toNat else False⊢ Day.mo < d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some d2this:if Day.tu ≤ d2 then steps + 1 = d2.toNat - Day.tu.toNat else False⊢ Day.tu < d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some d2this:if Day.we ≤ d2 then steps + 1 = d2.toNat - Day.we.toNat else False⊢ Day.we < d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some d2this:if Day.th ≤ d2 then steps + 1 = d2.toNat - Day.th.toNat else False⊢ Day.th < d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some d2this:if Day.fr ≤ d2 then steps + 1 = d2.toNat - Day.fr.toNat else False⊢ Day.fr < d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some d2this:if Day.sa ≤ d2 then steps + 1 = d2.toNat - Day.sa.toNat else False⊢ Day.sa < d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some d2this:if Day.su ≤ d2 then steps + 1 = d2.toNat - Day.su.toNat else False⊢ Day.su < d2 <;>mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some d2this:if Day.mo ≤ d2 then steps + 1 = d2.toNat - Day.mo.toNat else False⊢ Day.mo < d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some d2this:if Day.tu ≤ d2 then steps + 1 = d2.toNat - Day.tu.toNat else False⊢ Day.tu < d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some d2this:if Day.we ≤ d2 then steps + 1 = d2.toNat - Day.we.toNat else False⊢ Day.we < d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some d2this:if Day.th ≤ d2 then steps + 1 = d2.toNat - Day.th.toNat else False⊢ Day.th < d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some d2this:if Day.fr ≤ d2 then steps + 1 = d2.toNat - Day.fr.toNat else False⊢ Day.fr < d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some d2this:if Day.sa ≤ d2 then steps + 1 = d2.toNat - Day.sa.toNat else False⊢ Day.sa < d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some d2this:if Day.su ≤ d2 then steps + 1 = d2.toNat - Day.su.toNat else False⊢ Day.su < d2 cases d2mpr.su.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.su.toNat else False⊢ Day.su < Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.su.toNat else False⊢ Day.su < Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.wethis:if Day.su ≤ Day.we then steps + 1 = Day.we.toNat - Day.su.toNat else False⊢ Day.su < Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.ththis:if Day.su ≤ Day.th then steps + 1 = Day.th.toNat - Day.su.toNat else False⊢ Day.su < Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.su.toNat else False⊢ Day.su < Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.su.toNat else False⊢ Day.su < Day.sampr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:if Day.su ≤ Day.su then steps + 1 = Day.su.toNat - Day.su.toNat else False⊢ Day.su < Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.mothis:if Day.mo ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.mo.toNat else False⊢ Day.mo < Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.tuthis:if Day.mo ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.mo.toNat else False⊢ Day.mo < Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.wethis:if Day.mo ≤ Day.we then steps + 1 = Day.we.toNat - Day.mo.toNat else False⊢ Day.mo < Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.ththis:if Day.mo ≤ Day.th then steps + 1 = Day.th.toNat - Day.mo.toNat else False⊢ Day.mo < Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.frthis:if Day.mo ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.mo.toNat else False⊢ Day.mo < Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.sathis:if Day.mo ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.mo.toNat else False⊢ Day.mo < Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.suthis:if Day.mo ≤ Day.su then steps + 1 = Day.su.toNat - Day.mo.toNat else False⊢ Day.mo < Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.mothis:if Day.tu ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.tu.toNat else False⊢ Day.tu < Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.tuthis:if Day.tu ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.tu.toNat else False⊢ Day.tu < Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.wethis:if Day.tu ≤ Day.we then steps + 1 = Day.we.toNat - Day.tu.toNat else False⊢ Day.tu < Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.ththis:if Day.tu ≤ Day.th then steps + 1 = Day.th.toNat - Day.tu.toNat else False⊢ Day.tu < Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.frthis:if Day.tu ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.tu.toNat else False⊢ Day.tu < Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.sathis:if Day.tu ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.tu.toNat else False⊢ Day.tu < Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.suthis:if Day.tu ≤ Day.su then steps + 1 = Day.su.toNat - Day.tu.toNat else False⊢ Day.tu < Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.mothis:if Day.we ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.we.toNat else False⊢ Day.we < Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.tuthis:if Day.we ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.we.toNat else False⊢ Day.we < Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.wethis:if Day.we ≤ Day.we then steps + 1 = Day.we.toNat - Day.we.toNat else False⊢ Day.we < Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.ththis:if Day.we ≤ Day.th then steps + 1 = Day.th.toNat - Day.we.toNat else False⊢ Day.we < Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.frthis:if Day.we ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.we.toNat else False⊢ Day.we < Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.sathis:if Day.we ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.we.toNat else False⊢ Day.we < Day.sampr.we.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.suthis:if Day.we ≤ Day.su then steps + 1 = Day.su.toNat - Day.we.toNat else False⊢ Day.we < Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.mothis:if Day.th ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.th.toNat else False⊢ Day.th < Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.tuthis:if Day.th ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.th.toNat else False⊢ Day.th < Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.wethis:if Day.th ≤ Day.we then steps + 1 = Day.we.toNat - Day.th.toNat else False⊢ Day.th < Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.ththis:if Day.th ≤ Day.th then steps + 1 = Day.th.toNat - Day.th.toNat else False⊢ Day.th < Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.frthis:if Day.th ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.th.toNat else False⊢ Day.th < Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.sathis:if Day.th ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.th.toNat else False⊢ Day.th < Day.sampr.th.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.suthis:if Day.th ≤ Day.su then steps + 1 = Day.su.toNat - Day.th.toNat else False⊢ Day.th < Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.mothis:if Day.fr ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.fr.toNat else False⊢ Day.fr < Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.tuthis:if Day.fr ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.fr.toNat else False⊢ Day.fr < Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.wethis:if Day.fr ≤ Day.we then steps + 1 = Day.we.toNat - Day.fr.toNat else False⊢ Day.fr < Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.ththis:if Day.fr ≤ Day.th then steps + 1 = Day.th.toNat - Day.fr.toNat else False⊢ Day.fr < Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.frthis:if Day.fr ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.fr.toNat else False⊢ Day.fr < Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.sathis:if Day.fr ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.fr.toNat else False⊢ Day.fr < Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.suthis:if Day.fr ≤ Day.su then steps + 1 = Day.su.toNat - Day.fr.toNat else False⊢ Day.fr < Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.mothis:if Day.sa ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.sa.toNat else False⊢ Day.sa < Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.tuthis:if Day.sa ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.sa.toNat else False⊢ Day.sa < Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.wethis:if Day.sa ≤ Day.we then steps + 1 = Day.we.toNat - Day.sa.toNat else False⊢ Day.sa < Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.ththis:if Day.sa ≤ Day.th then steps + 1 = Day.th.toNat - Day.sa.toNat else False⊢ Day.sa < Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.frthis:if Day.sa ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.sa.toNat else False⊢ Day.sa < Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.sathis:if Day.sa ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.sa.toNat else False⊢ Day.sa < Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.suthis:if Day.sa ≤ Day.su then steps + 1 = Day.su.toNat - Day.sa.toNat else False⊢ Day.sa < Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.su.toNat else False⊢ Day.su < Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.su.toNat else False⊢ Day.su < Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.wethis:if Day.su ≤ Day.we then steps + 1 = Day.we.toNat - Day.su.toNat else False⊢ Day.su < Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.ththis:if Day.su ≤ Day.th then steps + 1 = Day.th.toNat - Day.su.toNat else False⊢ Day.su < Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.su.toNat else False⊢ Day.su < Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.su.toNat else False⊢ Day.su < Day.sampr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:if Day.su ≤ Day.su then steps + 1 = Day.su.toNat - Day.su.toNat else False⊢ Day.su < Day.su
      simp only [if_false_right] at thismpr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.mothis:Day.mo ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.mo.toNat⊢ Day.mo < Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.tuthis:Day.mo ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.mo.toNat⊢ Day.mo < Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.wethis:Day.mo ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.mo.toNat⊢ Day.mo < Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.ththis:Day.mo ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.mo.toNat⊢ Day.mo < Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.frthis:Day.mo ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.mo.toNat⊢ Day.mo < Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.sathis:Day.mo ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.mo.toNat⊢ Day.mo < Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.suthis:Day.mo ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.mo.toNat⊢ Day.mo < Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.mothis:Day.tu ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.tu.toNat⊢ Day.tu < Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.tuthis:Day.tu ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.tu.toNat⊢ Day.tu < Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.wethis:Day.tu ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.tu.toNat⊢ Day.tu < Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.ththis:Day.tu ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.tu.toNat⊢ Day.tu < Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.frthis:Day.tu ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.tu.toNat⊢ Day.tu < Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.sathis:Day.tu ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.tu.toNat⊢ Day.tu < Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.suthis:Day.tu ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.tu.toNat⊢ Day.tu < Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.mothis:Day.we ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.we.toNat⊢ Day.we < Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.tuthis:Day.we ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.we.toNat⊢ Day.we < Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.wethis:Day.we ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.we.toNat⊢ Day.we < Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.ththis:Day.we ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.we.toNat⊢ Day.we < Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.frthis:Day.we ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.we.toNat⊢ Day.we < Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.sathis:Day.we ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.we.toNat⊢ Day.we < Day.sampr.we.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.suthis:Day.we ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.we.toNat⊢ Day.we < Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.mothis:Day.th ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.th.toNat⊢ Day.th < Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.tuthis:Day.th ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.th.toNat⊢ Day.th < Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.wethis:Day.th ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.th.toNat⊢ Day.th < Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.ththis:Day.th ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.th.toNat⊢ Day.th < Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.frthis:Day.th ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.th.toNat⊢ Day.th < Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.sathis:Day.th ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.th.toNat⊢ Day.th < Day.sampr.th.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.suthis:Day.th ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.th.toNat⊢ Day.th < Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.mothis:Day.fr ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.fr.toNat⊢ Day.fr < Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.tuthis:Day.fr ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.fr.toNat⊢ Day.fr < Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.wethis:Day.fr ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.fr.toNat⊢ Day.fr < Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.ththis:Day.fr ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.fr.toNat⊢ Day.fr < Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.frthis:Day.fr ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.fr.toNat⊢ Day.fr < Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.sathis:Day.fr ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.fr.toNat⊢ Day.fr < Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.suthis:Day.fr ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.fr.toNat⊢ Day.fr < Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.mothis:Day.sa ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.sa.toNat⊢ Day.sa < Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.tuthis:Day.sa ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.sa.toNat⊢ Day.sa < Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.wethis:Day.sa ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.sa.toNat⊢ Day.sa < Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.ththis:Day.sa ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.sa.toNat⊢ Day.sa < Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.frthis:Day.sa ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.sa.toNat⊢ Day.sa < Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.sathis:Day.sa ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.sa.toNat⊢ Day.sa < Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.suthis:Day.sa ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.sa.toNat⊢ Day.sa < Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.mothis:Day.su ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.su.toNat⊢ Day.su < Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuthis:Day.su ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.su.toNat⊢ Day.su < Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.wethis:Day.su ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.su.toNat⊢ Day.su < Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.ththis:Day.su ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.su.toNat⊢ Day.su < Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frthis:Day.su ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.su.toNat⊢ Day.su < Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.sathis:Day.su ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.su.toNat⊢ Day.su < Day.sampr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su
      cases thismpr.su.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su <;>mpr.mo.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.moleft✝:Day.mo ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.mo.toNat⊢ Day.mo < Day.mompr.mo.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.tuleft✝:Day.mo ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.mo.toNat⊢ Day.mo < Day.tumpr.mo.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.weleft✝:Day.mo ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.mo.toNat⊢ Day.mo < Day.wempr.mo.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.thleft✝:Day.mo ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.mo.toNat⊢ Day.mo < Day.thmpr.mo.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.frleft✝:Day.mo ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.mo.toNat⊢ Day.mo < Day.frmpr.mo.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.saleft✝:Day.mo ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.mo.toNat⊢ Day.mo < Day.sampr.mo.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.suleft✝:Day.mo ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.mo.toNat⊢ Day.mo < Day.sumpr.tu.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.moleft✝:Day.tu ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.tu.toNat⊢ Day.tu < Day.mompr.tu.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.tuleft✝:Day.tu ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.tu.toNat⊢ Day.tu < Day.tumpr.tu.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.weleft✝:Day.tu ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.tu.toNat⊢ Day.tu < Day.wempr.tu.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.thleft✝:Day.tu ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.tu.toNat⊢ Day.tu < Day.thmpr.tu.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.frleft✝:Day.tu ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.tu.toNat⊢ Day.tu < Day.frmpr.tu.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.saleft✝:Day.tu ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.tu.toNat⊢ Day.tu < Day.sampr.tu.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.suleft✝:Day.tu ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.tu.toNat⊢ Day.tu < Day.sumpr.we.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.moleft✝:Day.we ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.we.toNat⊢ Day.we < Day.mompr.we.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.tuleft✝:Day.we ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.we.toNat⊢ Day.we < Day.tumpr.we.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.weleft✝:Day.we ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.we.toNat⊢ Day.we < Day.wempr.we.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.thleft✝:Day.we ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.we.toNat⊢ Day.we < Day.thmpr.we.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.frleft✝:Day.we ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.we.toNat⊢ Day.we < Day.frmpr.we.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.saleft✝:Day.we ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.we.toNat⊢ Day.we < Day.sampr.we.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.suleft✝:Day.we ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.we.toNat⊢ Day.we < Day.sumpr.th.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.moleft✝:Day.th ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.th.toNat⊢ Day.th < Day.mompr.th.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.tuleft✝:Day.th ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.th.toNat⊢ Day.th < Day.tumpr.th.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.weleft✝:Day.th ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.th.toNat⊢ Day.th < Day.wempr.th.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.thleft✝:Day.th ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.th.toNat⊢ Day.th < Day.thmpr.th.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.frleft✝:Day.th ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.th.toNat⊢ Day.th < Day.frmpr.th.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.saleft✝:Day.th ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.th.toNat⊢ Day.th < Day.sampr.th.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.suleft✝:Day.th ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.th.toNat⊢ Day.th < Day.sumpr.fr.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.moleft✝:Day.fr ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.fr.toNat⊢ Day.fr < Day.mompr.fr.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.tuleft✝:Day.fr ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.fr.toNat⊢ Day.fr < Day.tumpr.fr.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.weleft✝:Day.fr ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.fr.toNat⊢ Day.fr < Day.wempr.fr.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.thleft✝:Day.fr ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.fr.toNat⊢ Day.fr < Day.thmpr.fr.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.frleft✝:Day.fr ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.fr.toNat⊢ Day.fr < Day.frmpr.fr.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.saleft✝:Day.fr ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.fr.toNat⊢ Day.fr < Day.sampr.fr.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.suleft✝:Day.fr ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.fr.toNat⊢ Day.fr < Day.sumpr.sa.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.moleft✝:Day.sa ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.sa.toNat⊢ Day.sa < Day.mompr.sa.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.tuleft✝:Day.sa ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.sa.toNat⊢ Day.sa < Day.tumpr.sa.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.weleft✝:Day.sa ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.sa.toNat⊢ Day.sa < Day.wempr.sa.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.thleft✝:Day.sa ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.sa.toNat⊢ Day.sa < Day.thmpr.sa.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.frleft✝:Day.sa ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.sa.toNat⊢ Day.sa < Day.frmpr.sa.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.saleft✝:Day.sa ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.sa.toNat⊢ Day.sa < Day.sampr.sa.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.suleft✝:Day.sa ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.sa.toNat⊢ Day.sa < Day.sumpr.su.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.moleft✝:Day.su ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.su.toNat⊢ Day.su < Day.mompr.su.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuleft✝:Day.su ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.su.toNat⊢ Day.su < Day.tumpr.su.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.weleft✝:Day.su ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.su.toNat⊢ Day.su < Day.wempr.su.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.thleft✝:Day.su ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.su.toNat⊢ Day.su < Day.thmpr.su.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frleft✝:Day.su ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.su.toNat⊢ Day.su < Day.frmpr.su.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.saleft✝:Day.su ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.su.toNat⊢ Day.su < Day.sampr.su.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su first | decidempr.su.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su | contradictionAll goals completed! 🐙

instance : Std.PRange.LawfulUpwardEnumerableLE Day where
  le_iff d1 d2 := byd1:Dayd2:Day⊢ d1 ≤ d2 ↔ Std.PRange.UpwardEnumerable.LE d1 d2
    constructormpd1:Dayd2:Day⊢ d1 ≤ d2 → Std.PRange.UpwardEnumerable.LE d1 d2mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LE d1 d2 → d1 ≤ d2
    .mpd1:Dayd2:Day⊢ d1 ≤ d2 → Std.PRange.UpwardEnumerable.LE d1 d2 intro lempd1:Dayd2:Dayle:d1 ≤ d2⊢ Std.PRange.UpwardEnumerable.LE d1 d2
      simp only [Std.PRange.UpwardEnumerable.LE]mpd1:Dayd2:Dayle:d1 ≤ d2⊢ ∃ n, Std.PRange.succMany? n d1 = some d2
      exists d2.toNat - d1.toNatmpd1:Dayd2:Dayle:d1 ≤ d2⊢ Std.PRange.succMany? (d2.toNat - d1.toNat) d1 = some d2
      cases d1mp.mod2:Dayle:Day.mo ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.mo.toNat) Day.mo = some d2mp.tud2:Dayle:Day.tu ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.tu.toNat) Day.tu = some d2mp.wed2:Dayle:Day.we ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.we.toNat) Day.we = some d2mp.thd2:Dayle:Day.th ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.th.toNat) Day.th = some d2mp.frd2:Dayle:Day.fr ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.fr.toNat) Day.fr = some d2mp.sad2:Dayle:Day.sa ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.sa.toNat) Day.sa = some d2mp.sud2:Dayle:Day.su ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.su.toNat) Day.su = some d2 <;>mp.mod2:Dayle:Day.mo ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.mo.toNat) Day.mo = some d2mp.tud2:Dayle:Day.tu ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.tu.toNat) Day.tu = some d2mp.wed2:Dayle:Day.we ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.we.toNat) Day.we = some d2mp.thd2:Dayle:Day.th ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.th.toNat) Day.th = some d2mp.frd2:Dayle:Day.fr ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.fr.toNat) Day.fr = some d2mp.sad2:Dayle:Day.sa ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.sa.toNat) Day.sa = some d2mp.sud2:Dayle:Day.su ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.su.toNat) Day.su = some d2 cases d2mp.su.mole:Day.su ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat) Day.su = some Day.momp.su.tule:Day.su ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat) Day.su = some Day.tump.su.wele:Day.su ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.su.toNat) Day.su = some Day.wemp.su.thle:Day.su ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.su.toNat) Day.su = some Day.thmp.su.frle:Day.su ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat) Day.su = some Day.frmp.su.sale:Day.su ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat) Day.su = some Day.samp.su.sule:Day.su ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.su.toNat) Day.su = some Day.su <;>mp.mo.mole:Day.mo ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.mo.toNat) Day.mo = some Day.momp.mo.tule:Day.mo ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.mo.toNat) Day.mo = some Day.tump.mo.wele:Day.mo ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.mo.toNat) Day.mo = some Day.wemp.mo.thle:Day.mo ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.mo.toNat) Day.mo = some Day.thmp.mo.frle:Day.mo ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.mo.toNat) Day.mo = some Day.frmp.mo.sale:Day.mo ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.mo.toNat) Day.mo = some Day.samp.mo.sule:Day.mo ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.mo.toNat) Day.mo = some Day.sump.tu.mole:Day.tu ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.tu.toNat) Day.tu = some Day.momp.tu.tule:Day.tu ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.tu.toNat) Day.tu = some Day.tump.tu.wele:Day.tu ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.tu.toNat) Day.tu = some Day.wemp.tu.thle:Day.tu ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.tu.toNat) Day.tu = some Day.thmp.tu.frle:Day.tu ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.tu.toNat) Day.tu = some Day.frmp.tu.sale:Day.tu ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.tu.toNat) Day.tu = some Day.samp.tu.sule:Day.tu ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.tu.toNat) Day.tu = some Day.sump.we.mole:Day.we ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.we.toNat) Day.we = some Day.momp.we.tule:Day.we ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.we.toNat) Day.we = some Day.tump.we.wele:Day.we ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.we.toNat) Day.we = some Day.wemp.we.thle:Day.we ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.we.toNat) Day.we = some Day.thmp.we.frle:Day.we ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.we.toNat) Day.we = some Day.frmp.we.sale:Day.we ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.we.toNat) Day.we = some Day.samp.we.sule:Day.we ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.we.toNat) Day.we = some Day.sump.th.mole:Day.th ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.th.toNat) Day.th = some Day.momp.th.tule:Day.th ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.th.toNat) Day.th = some Day.tump.th.wele:Day.th ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.th.toNat) Day.th = some Day.wemp.th.thle:Day.th ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.th.toNat) Day.th = some Day.thmp.th.frle:Day.th ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.th.toNat) Day.th = some Day.frmp.th.sale:Day.th ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.th.toNat) Day.th = some Day.samp.th.sule:Day.th ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.th.toNat) Day.th = some Day.sump.fr.mole:Day.fr ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.fr.toNat) Day.fr = some Day.momp.fr.tule:Day.fr ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.fr.toNat) Day.fr = some Day.tump.fr.wele:Day.fr ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.fr.toNat) Day.fr = some Day.wemp.fr.thle:Day.fr ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.fr.toNat) Day.fr = some Day.thmp.fr.frle:Day.fr ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.fr.toNat) Day.fr = some Day.frmp.fr.sale:Day.fr ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.fr.toNat) Day.fr = some Day.samp.fr.sule:Day.fr ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.fr.toNat) Day.fr = some Day.sump.sa.mole:Day.sa ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.sa.toNat) Day.sa = some Day.momp.sa.tule:Day.sa ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.sa.toNat) Day.sa = some Day.tump.sa.wele:Day.sa ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.sa.toNat) Day.sa = some Day.wemp.sa.thle:Day.sa ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.sa.toNat) Day.sa = some Day.thmp.sa.frle:Day.sa ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.sa.toNat) Day.sa = some Day.frmp.sa.sale:Day.sa ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.sa.toNat) Day.sa = some Day.samp.sa.sule:Day.sa ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.sa.toNat) Day.sa = some Day.sump.su.mole:Day.su ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat) Day.su = some Day.momp.su.tule:Day.su ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat) Day.su = some Day.tump.su.wele:Day.su ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.su.toNat) Day.su = some Day.wemp.su.thle:Day.su ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.su.toNat) Day.su = some Day.thmp.su.frle:Day.su ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat) Day.su = some Day.frmp.su.sale:Day.su ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat) Day.su = some Day.samp.su.sule:Day.su ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.su.toNat) Day.su = some Day.su
      simp_all [Day.toNat, Std.PRange.succ?, Day.succ?]All goals completed! 🐙 <;>mp.tu.mole:Day.tu ≤ Day.mo⊢ Falsemp.we.mole:Day.we ≤ Day.mo⊢ Falsemp.we.tule:Day.we ≤ Day.tu⊢ Falsemp.th.mole:Day.th ≤ Day.mo⊢ Falsemp.th.tule:Day.th ≤ Day.tu⊢ Falsemp.th.wele:Day.th ≤ Day.we⊢ Falsemp.fr.mole:Day.fr ≤ Day.mo⊢ Falsemp.fr.tule:Day.fr ≤ Day.tu⊢ Falsemp.fr.wele:Day.fr ≤ Day.we⊢ Falsemp.fr.thle:Day.fr ≤ Day.th⊢ Falsemp.sa.mole:Day.sa ≤ Day.mo⊢ Falsemp.sa.tule:Day.sa ≤ Day.tu⊢ Falsemp.sa.wele:Day.sa ≤ Day.we⊢ Falsemp.sa.thle:Day.sa ≤ Day.th⊢ Falsemp.sa.frle:Day.sa ≤ Day.fr⊢ Falsemp.su.mole:Day.su ≤ Day.mo⊢ Falsemp.su.tule:Day.su ≤ Day.tu⊢ Falsemp.su.wele:Day.su ≤ Day.we⊢ Falsemp.su.thle:Day.su ≤ Day.th⊢ Falsemp.su.frle:Day.su ≤ Day.fr⊢ Falsemp.su.sale:Day.su ≤ Day.sa⊢ False
      contradictionAll goals completed! 🐙
    .mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LE d1 d2 → d1 ≤ d2 intro ⟨steps, eq⟩mprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? steps d1 = some d2⊢ d1 ≤ d2
      have := Day.succMany?_steps eqmprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? steps d1 = some d2this:if d1 ≤ d2 then steps = d2.toNat - d1.toNat else False⊢ d1 ≤ d2
      cases d1mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? steps Day.mo = some d2this:if Day.mo ≤ d2 then steps = d2.toNat - Day.mo.toNat else False⊢ Day.mo ≤ d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.tu = some d2this:if Day.tu ≤ d2 then steps = d2.toNat - Day.tu.toNat else False⊢ Day.tu ≤ d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? steps Day.we = some d2this:if Day.we ≤ d2 then steps = d2.toNat - Day.we.toNat else False⊢ Day.we ≤ d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.th = some d2this:if Day.th ≤ d2 then steps = d2.toNat - Day.th.toNat else False⊢ Day.th ≤ d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.fr = some d2this:if Day.fr ≤ d2 then steps = d2.toNat - Day.fr.toNat else False⊢ Day.fr ≤ d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? steps Day.sa = some d2this:if Day.sa ≤ d2 then steps = d2.toNat - Day.sa.toNat else False⊢ Day.sa ≤ d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.su = some d2this:if Day.su ≤ d2 then steps = d2.toNat - Day.su.toNat else False⊢ Day.su ≤ d2 <;>mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? steps Day.mo = some d2this:if Day.mo ≤ d2 then steps = d2.toNat - Day.mo.toNat else False⊢ Day.mo ≤ d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.tu = some d2this:if Day.tu ≤ d2 then steps = d2.toNat - Day.tu.toNat else False⊢ Day.tu ≤ d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? steps Day.we = some d2this:if Day.we ≤ d2 then steps = d2.toNat - Day.we.toNat else False⊢ Day.we ≤ d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.th = some d2this:if Day.th ≤ d2 then steps = d2.toNat - Day.th.toNat else False⊢ Day.th ≤ d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.fr = some d2this:if Day.fr ≤ d2 then steps = d2.toNat - Day.fr.toNat else False⊢ Day.fr ≤ d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? steps Day.sa = some d2this:if Day.sa ≤ d2 then steps = d2.toNat - Day.sa.toNat else False⊢ Day.sa ≤ d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.su = some d2this:if Day.su ≤ d2 then steps = d2.toNat - Day.su.toNat else False⊢ Day.su ≤ d2 cases d2mpr.su.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps = Day.mo.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps = Day.tu.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.wethis:if Day.su ≤ Day.we then steps = Day.we.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.ththis:if Day.su ≤ Day.th then steps = Day.th.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps = Day.fr.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps = Day.sa.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.sampr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:if Day.su ≤ Day.su then steps = Day.su.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.mothis:if Day.mo ≤ Day.mo then steps = Day.mo.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuthis:if Day.mo ≤ Day.tu then steps = Day.tu.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.wethis:if Day.mo ≤ Day.we then steps = Day.we.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.ththis:if Day.mo ≤ Day.th then steps = Day.th.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frthis:if Day.mo ≤ Day.fr then steps = Day.fr.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.sathis:if Day.mo ≤ Day.sa then steps = Day.sa.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suthis:if Day.mo ≤ Day.su then steps = Day.su.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.mothis:if Day.tu ≤ Day.mo then steps = Day.mo.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuthis:if Day.tu ≤ Day.tu then steps = Day.tu.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.wethis:if Day.tu ≤ Day.we then steps = Day.we.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.ththis:if Day.tu ≤ Day.th then steps = Day.th.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frthis:if Day.tu ≤ Day.fr then steps = Day.fr.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.sathis:if Day.tu ≤ Day.sa then steps = Day.sa.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suthis:if Day.tu ≤ Day.su then steps = Day.su.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.mothis:if Day.we ≤ Day.mo then steps = Day.mo.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuthis:if Day.we ≤ Day.tu then steps = Day.tu.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? steps Day.we = some Day.wethis:if Day.we ≤ Day.we then steps = Day.we.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.ththis:if Day.we ≤ Day.th then steps = Day.th.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frthis:if Day.we ≤ Day.fr then steps = Day.fr.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.sathis:if Day.we ≤ Day.sa then steps = Day.sa.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.sampr.we.susteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suthis:if Day.we ≤ Day.su then steps = Day.su.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.mothis:if Day.th ≤ Day.mo then steps = Day.mo.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuthis:if Day.th ≤ Day.tu then steps = Day.tu.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? steps Day.th = some Day.wethis:if Day.th ≤ Day.we then steps = Day.we.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.ththis:if Day.th ≤ Day.th then steps = Day.th.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frthis:if Day.th ≤ Day.fr then steps = Day.fr.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.sathis:if Day.th ≤ Day.sa then steps = Day.sa.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.sampr.th.susteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suthis:if Day.th ≤ Day.su then steps = Day.su.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.mothis:if Day.fr ≤ Day.mo then steps = Day.mo.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuthis:if Day.fr ≤ Day.tu then steps = Day.tu.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.wethis:if Day.fr ≤ Day.we then steps = Day.we.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.ththis:if Day.fr ≤ Day.th then steps = Day.th.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frthis:if Day.fr ≤ Day.fr then steps = Day.fr.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.sathis:if Day.fr ≤ Day.sa then steps = Day.sa.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suthis:if Day.fr ≤ Day.su then steps = Day.su.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.mothis:if Day.sa ≤ Day.mo then steps = Day.mo.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuthis:if Day.sa ≤ Day.tu then steps = Day.tu.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.wethis:if Day.sa ≤ Day.we then steps = Day.we.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.ththis:if Day.sa ≤ Day.th then steps = Day.th.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frthis:if Day.sa ≤ Day.fr then steps = Day.fr.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.sathis:if Day.sa ≤ Day.sa then steps = Day.sa.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suthis:if Day.sa ≤ Day.su then steps = Day.su.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps = Day.mo.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps = Day.tu.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.wethis:if Day.su ≤ Day.we then steps = Day.we.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.ththis:if Day.su ≤ Day.th then steps = Day.th.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps = Day.fr.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps = Day.sa.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.sampr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:if Day.su ≤ Day.su then steps = Day.su.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.su
      simp only [if_false_right] at thismpr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.mothis:Day.mo ≤ Day.mo ∧ steps = Day.mo.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuthis:Day.mo ≤ Day.tu ∧ steps = Day.tu.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.wethis:Day.mo ≤ Day.we ∧ steps = Day.we.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.ththis:Day.mo ≤ Day.th ∧ steps = Day.th.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frthis:Day.mo ≤ Day.fr ∧ steps = Day.fr.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.sathis:Day.mo ≤ Day.sa ∧ steps = Day.sa.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suthis:Day.mo ≤ Day.su ∧ steps = Day.su.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.mothis:Day.tu ≤ Day.mo ∧ steps = Day.mo.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuthis:Day.tu ≤ Day.tu ∧ steps = Day.tu.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.wethis:Day.tu ≤ Day.we ∧ steps = Day.we.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.ththis:Day.tu ≤ Day.th ∧ steps = Day.th.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frthis:Day.tu ≤ Day.fr ∧ steps = Day.fr.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.sathis:Day.tu ≤ Day.sa ∧ steps = Day.sa.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suthis:Day.tu ≤ Day.su ∧ steps = Day.su.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.mothis:Day.we ≤ Day.mo ∧ steps = Day.mo.toNat - Day.we.toNat⊢ Day.we ≤ Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuthis:Day.we ≤ Day.tu ∧ steps = Day.tu.toNat - Day.we.toNat⊢ Day.we ≤ Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? steps Day.we = some Day.wethis:Day.we ≤ Day.we ∧ steps = Day.we.toNat - Day.we.toNat⊢ Day.we ≤ Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.ththis:Day.we ≤ Day.th ∧ steps = Day.th.toNat - Day.we.toNat⊢ Day.we ≤ Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frthis:Day.we ≤ Day.fr ∧ steps = Day.fr.toNat - Day.we.toNat⊢ Day.we ≤ Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.sathis:Day.we ≤ Day.sa ∧ steps = Day.sa.toNat - Day.we.toNat⊢ Day.we ≤ Day.sampr.we.susteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suthis:Day.we ≤ Day.su ∧ steps = Day.su.toNat - Day.we.toNat⊢ Day.we ≤ Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.mothis:Day.th ≤ Day.mo ∧ steps = Day.mo.toNat - Day.th.toNat⊢ Day.th ≤ Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuthis:Day.th ≤ Day.tu ∧ steps = Day.tu.toNat - Day.th.toNat⊢ Day.th ≤ Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? steps Day.th = some Day.wethis:Day.th ≤ Day.we ∧ steps = Day.we.toNat - Day.th.toNat⊢ Day.th ≤ Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.ththis:Day.th ≤ Day.th ∧ steps = Day.th.toNat - Day.th.toNat⊢ Day.th ≤ Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frthis:Day.th ≤ Day.fr ∧ steps = Day.fr.toNat - Day.th.toNat⊢ Day.th ≤ Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.sathis:Day.th ≤ Day.sa ∧ steps = Day.sa.toNat - Day.th.toNat⊢ Day.th ≤ Day.sampr.th.susteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suthis:Day.th ≤ Day.su ∧ steps = Day.su.toNat - Day.th.toNat⊢ Day.th ≤ Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.mothis:Day.fr ≤ Day.mo ∧ steps = Day.mo.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuthis:Day.fr ≤ Day.tu ∧ steps = Day.tu.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.wethis:Day.fr ≤ Day.we ∧ steps = Day.we.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.ththis:Day.fr ≤ Day.th ∧ steps = Day.th.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frthis:Day.fr ≤ Day.fr ∧ steps = Day.fr.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.sathis:Day.fr ≤ Day.sa ∧ steps = Day.sa.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suthis:Day.fr ≤ Day.su ∧ steps = Day.su.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.mothis:Day.sa ≤ Day.mo ∧ steps = Day.mo.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuthis:Day.sa ≤ Day.tu ∧ steps = Day.tu.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.wethis:Day.sa ≤ Day.we ∧ steps = Day.we.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.ththis:Day.sa ≤ Day.th ∧ steps = Day.th.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frthis:Day.sa ≤ Day.fr ∧ steps = Day.fr.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.sathis:Day.sa ≤ Day.sa ∧ steps = Day.sa.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suthis:Day.sa ≤ Day.su ∧ steps = Day.su.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.mothis:Day.su ≤ Day.mo ∧ steps = Day.mo.toNat - Day.su.toNat⊢ Day.su ≤ Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuthis:Day.su ≤ Day.tu ∧ steps = Day.tu.toNat - Day.su.toNat⊢ Day.su ≤ Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.wethis:Day.su ≤ Day.we ∧ steps = Day.we.toNat - Day.su.toNat⊢ Day.su ≤ Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.ththis:Day.su ≤ Day.th ∧ steps = Day.th.toNat - Day.su.toNat⊢ Day.su ≤ Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frthis:Day.su ≤ Day.fr ∧ steps = Day.fr.toNat - Day.su.toNat⊢ Day.su ≤ Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.sathis:Day.su ≤ Day.sa ∧ steps = Day.sa.toNat - Day.su.toNat⊢ Day.su ≤ Day.sampr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su
      cases thismpr.su.su.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su <;>mpr.mo.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.moleft✝:Day.mo ≤ Day.moright✝:steps = Day.mo.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.mompr.mo.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuleft✝:Day.mo ≤ Day.turight✝:steps = Day.tu.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.tumpr.mo.we.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.weleft✝:Day.mo ≤ Day.weright✝:steps = Day.we.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.wempr.mo.th.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.thleft✝:Day.mo ≤ Day.thright✝:steps = Day.th.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.thmpr.mo.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frleft✝:Day.mo ≤ Day.frright✝:steps = Day.fr.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.frmpr.mo.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.saleft✝:Day.mo ≤ Day.saright✝:steps = Day.sa.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sampr.mo.su.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suleft✝:Day.mo ≤ Day.suright✝:steps = Day.su.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sumpr.tu.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.moleft✝:Day.tu ≤ Day.moright✝:steps = Day.mo.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.mompr.tu.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuleft✝:Day.tu ≤ Day.turight✝:steps = Day.tu.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.tumpr.tu.we.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.weleft✝:Day.tu ≤ Day.weright✝:steps = Day.we.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.wempr.tu.th.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.thleft✝:Day.tu ≤ Day.thright✝:steps = Day.th.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.thmpr.tu.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frleft✝:Day.tu ≤ Day.frright✝:steps = Day.fr.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.frmpr.tu.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.saleft✝:Day.tu ≤ Day.saright✝:steps = Day.sa.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sampr.tu.su.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suleft✝:Day.tu ≤ Day.suright✝:steps = Day.su.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sumpr.we.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.moleft✝:Day.we ≤ Day.moright✝:steps = Day.mo.toNat - Day.we.toNat⊢ Day.we ≤ Day.mompr.we.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuleft✝:Day.we ≤ Day.turight✝:steps = Day.tu.toNat - Day.we.toNat⊢ Day.we ≤ Day.tumpr.we.we.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.weleft✝:Day.we ≤ Day.weright✝:steps = Day.we.toNat - Day.we.toNat⊢ Day.we ≤ Day.wempr.we.th.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.thleft✝:Day.we ≤ Day.thright✝:steps = Day.th.toNat - Day.we.toNat⊢ Day.we ≤ Day.thmpr.we.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frleft✝:Day.we ≤ Day.frright✝:steps = Day.fr.toNat - Day.we.toNat⊢ Day.we ≤ Day.frmpr.we.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.saleft✝:Day.we ≤ Day.saright✝:steps = Day.sa.toNat - Day.we.toNat⊢ Day.we ≤ Day.sampr.we.su.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suleft✝:Day.we ≤ Day.suright✝:steps = Day.su.toNat - Day.we.toNat⊢ Day.we ≤ Day.sumpr.th.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.moleft✝:Day.th ≤ Day.moright✝:steps = Day.mo.toNat - Day.th.toNat⊢ Day.th ≤ Day.mompr.th.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuleft✝:Day.th ≤ Day.turight✝:steps = Day.tu.toNat - Day.th.toNat⊢ Day.th ≤ Day.tumpr.th.we.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.weleft✝:Day.th ≤ Day.weright✝:steps = Day.we.toNat - Day.th.toNat⊢ Day.th ≤ Day.wempr.th.th.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.thleft✝:Day.th ≤ Day.thright✝:steps = Day.th.toNat - Day.th.toNat⊢ Day.th ≤ Day.thmpr.th.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frleft✝:Day.th ≤ Day.frright✝:steps = Day.fr.toNat - Day.th.toNat⊢ Day.th ≤ Day.frmpr.th.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.saleft✝:Day.th ≤ Day.saright✝:steps = Day.sa.toNat - Day.th.toNat⊢ Day.th ≤ Day.sampr.th.su.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suleft✝:Day.th ≤ Day.suright✝:steps = Day.su.toNat - Day.th.toNat⊢ Day.th ≤ Day.sumpr.fr.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.moleft✝:Day.fr ≤ Day.moright✝:steps = Day.mo.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.mompr.fr.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuleft✝:Day.fr ≤ Day.turight✝:steps = Day.tu.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.tumpr.fr.we.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.weleft✝:Day.fr ≤ Day.weright✝:steps = Day.we.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.wempr.fr.th.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.thleft✝:Day.fr ≤ Day.thright✝:steps = Day.th.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.thmpr.fr.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frleft✝:Day.fr ≤ Day.frright✝:steps = Day.fr.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.frmpr.fr.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.saleft✝:Day.fr ≤ Day.saright✝:steps = Day.sa.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sampr.fr.su.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suleft✝:Day.fr ≤ Day.suright✝:steps = Day.su.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sumpr.sa.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.moleft✝:Day.sa ≤ Day.moright✝:steps = Day.mo.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.mompr.sa.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuleft✝:Day.sa ≤ Day.turight✝:steps = Day.tu.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.tumpr.sa.we.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.weleft✝:Day.sa ≤ Day.weright✝:steps = Day.we.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.wempr.sa.th.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.thleft✝:Day.sa ≤ Day.thright✝:steps = Day.th.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.thmpr.sa.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frleft✝:Day.sa ≤ Day.frright✝:steps = Day.fr.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.frmpr.sa.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.saleft✝:Day.sa ≤ Day.saright✝:steps = Day.sa.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sampr.sa.su.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suleft✝:Day.sa ≤ Day.suright✝:steps = Day.su.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sumpr.su.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.moleft✝:Day.su ≤ Day.moright✝:steps = Day.mo.toNat - Day.su.toNat⊢ Day.su ≤ Day.mompr.su.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuleft✝:Day.su ≤ Day.turight✝:steps = Day.tu.toNat - Day.su.toNat⊢ Day.su ≤ Day.tumpr.su.we.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.weleft✝:Day.su ≤ Day.weright✝:steps = Day.we.toNat - Day.su.toNat⊢ Day.su ≤ Day.wempr.su.th.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.thleft✝:Day.su ≤ Day.thright✝:steps = Day.th.toNat - Day.su.toNat⊢ Day.su ≤ Day.thmpr.su.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frleft✝:Day.su ≤ Day.frright✝:steps = Day.fr.toNat - Day.su.toNat⊢ Day.su ≤ Day.frmpr.su.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.saleft✝:Day.su ≤ Day.saright✝:steps = Day.sa.toNat - Day.su.toNat⊢ Day.su ≤ Day.sampr.su.su.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su grindAll goals completed! 🐙

现在可以迭代天数范围：

It's Day.mo
It's Day.tu
It's Day.we
#eval show IO Unit from do
  for x in (Day.mo...Day.th).iter do
    IO.println s!"It's {repr x}"

It's Day.mo
It's Day.tu
It's Day.we

Live ↪

20.18.4. 范围和切片🔗

范围语法可与支持切片的数据结构一起使用以选择结构的切片。

Slicing Lists

列表可以使用任何间隔类型进行切片：

def groceries :=
  ["apples", "bananas", "coffee", "dates", "endive", "fennel"]

["bananas", "coffee", "dates"]#eval groceries[1...4] |>.toList

["bananas", "coffee", "dates"]

["bananas", "coffee", "dates", "endive"]#eval groceries[1...=4] |>.toList

["bananas", "coffee", "dates", "endive"]

["bananas", "coffee", "dates", "endive", "fennel"]#eval groceries[1...*] |>.toList

["bananas", "coffee", "dates", "endive", "fennel"]

["coffee", "dates"]#eval groceries[1<...4] |>.toList

["coffee", "dates"]

["coffee", "dates", "endive"]#eval groceries[1<...=4] |>.toList

["coffee", "dates", "endive"]

["apples", "bananas", "coffee", "dates", "endive"]#eval groceries[*...=4] |>.toList

["apples", "bananas", "coffee", "dates", "endive"]

["apples", "bananas", "coffee", "dates"]#eval groceries[*...4] |>.toList

["apples", "bananas", "coffee", "dates"]

["apples", "bananas", "coffee", "dates", "endive", "fennel"]#eval groceries[*...*] |>.toList

["apples", "bananas", "coffee", "dates", "endive", "fennel"]

Live ↪

Custom Slices

Triple 包含三个相同类型的值：

structure Triple (α : Type u) where
  fst : α
  snd : α
  thd : α
deriving Repr

三元组中的位置可以是任何字段，或者紧接在 thd 之后：

inductive TriplePos where
  | fst | snd | thd | done
deriving Repr

三元组的切片由三元组、起始位置和停止位置组成。包含起始位置，不包含停止位置：

structure TripleSlice (α : Type u) where
  triple : Triple α
  start : TriplePos
  stop : TriplePos
deriving Repr

通过实现每个支持的范围类型的 Sliceable 类的实例，TriplePos 的范围可用于从三元组中选择一个切片。例如，Std.Rco.Sliceable 允许使用左闭、右开范围对 Triple 进行切片：

instance : Std.Rco.Sliceable (Triple α) TriplePos (TripleSlice α) where
  mkSlice triple range :=
    { triple, start := range.lower, stop := range.upper }

def abc : Triple Char := ⟨'a', 'b', 'c'⟩

open TriplePos in
{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.thd }#eval abc[snd...thd]

{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.thd }

无限范围只有一个下界：

instance : Std.Rci.Sliceable (Triple α) TriplePos (TripleSlice α) where
  mkSlice triple range :=
    { triple, start := range.lower, stop := .done }

open TriplePos in
{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.done }#eval abc[snd...*]

{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.done }

Live ↪

type class

Std.Rco.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rco.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-closed right-open.

The type of the resulting slices is γ.

Instance Constructor

Std.Rco.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Rco β → γ

Slices carrier from range.lower (inclusive) to range.upper (exclusive).

type class

Std.Rcc.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rcc.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being closed.

The type of the resulting slices is γ.

Instance Constructor

Std.Rcc.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Rcc β → γ

Slices carrier from range.lower to range.upper, both inclusive.

type class

Std.Rci.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rci.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-closed right-unbounded.

The type of the resulting slices is γ.

Instance Constructor

Std.Rci.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Rci β → γ

Slices carrier from range.lower (inclusive).

type class

Std.Roo.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Roo.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being open.

The type of the resulting slices is γ.

Instance Constructor

Std.Roo.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Roo β → γ

Slices carrier from range.lower to range.upper, both exclusive.

type class

Std.Roc.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Roc.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-open right-closed.

The type of the resulting slices is γ.

Instance Constructor

Std.Roc.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Roc β → γ

Slices carrier from range.lower (exclusive) to range.upper (inclusive).

type class

Std.Roi.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Roi.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-open right-unbounded.

The type of the resulting slices is γ.

Instance Constructor

Std.Roi.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Roi β → γ

Slices carrier from range.lower (exclusive).

type class

Std.Rio.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rio.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-unbounded right-open.

The type of the resulting slices is γ.

Instance Constructor

Std.Rio.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Rio β → γ

Slices carrier up to range.upper (exclusive).

type class

Std.Ric.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Ric.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-unbounded right-closed.

The type of the resulting slices is γ.

Instance Constructor

Std.Ric.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Ric β → γ

Slices carrier up to range.upper (inclusive).

type class

Std.Rii.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max u w)
Std.Rii.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max u w)

This typeclass indicates how to obtain slices of elements of α over the full range in the index type β.

The type of the resulting slices is γ.

Instance Constructor

Std.Rii.Sliceable.mk.{u, v, w}

Methods

mkSlice : α → Std.Rii β → γ

Slices carrier with no bounds.

20.1.	自然数
20.2.	整数
20.3.	有限自然数
20.4.	固定精度整数
20.5.	位提供
20.6.	浮点数
20.7.	人物
20.8.	弦乐
20.9.	单位 Type
20.10.	空的Type
20.11.	布尔值
20.12.	任选值
20.13.	元组
20.14.	总和类型
20.15.	链表
20.16.	储备
20.17.	字节吞吐量
20.18.	范围
20.19.	地图和套装
20.20.	亚型
20.21.	调用计算