`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitZeroLtOne`

IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/RatioOrbitZeroLtOne.lean · 25 lines · 1 declarations

Explainer status: pending

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLtTrichotomy
   5import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
   6
   7namespace IndisputableMonolith.PRCGrow.RatioOrbitZeroLtOne
   8
   9open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
  10open IndisputableMonolith.PRCGrow.RatioOrbitLtTrichotomy
  11open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  12open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  13
  14theorem zero_ltQ_one : ltQ RatioOrbit.zero RatioOrbit.one := by
  15  unfold ltQ
  16  refine ⟨?_, ?_⟩
  17  · unfold leQ
  18    rw [le_iff_toNat_cf]
  19    decide
  20  · intro h
  21    have hf : ¬ RatioOrbit.crossEq RatioOrbit.zero RatioOrbit.one := by decide
  22    exact hf h
  23
  24end IndisputableMonolith.PRCGrow.RatioOrbitZeroLtOne
  25

source mirrored from github.com/jonwashburn/shape-of-logic