theorem proved term proof

`ordered_interpret_le_iff`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  83theorem ordered_interpret_le_iff (a b : ArithmeticFromLogic.LogicNat) :
  84    ArithmeticFromLogic.LogicNat.toNat a ≤ ArithmeticFromLogic.LogicNat.toNat b ↔ a ≤ b := by

proof body

Term-mode proof.

  85  exact (ArithmeticFromLogic.LogicNat.toNat_le a b).symm
  86
  87end OrderedLogicRealization
  88end Foundation
  89end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.

LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_le in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use