`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrRightOfBalancedChoiceFree`

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

show as: view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
   5import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
   6
   7namespace IndisputableMonolith.PRCGrow.SignedOrbitLeCongrRightOfBalancedChoiceFree
   8
   9open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  10open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  11
  12theorem le_congr_right_of_balanced_cf {a b b' : SignedOrbit}
  13    (h : b.balanced b') :
  14    a.le b ↔ a.le b' := by
  15  rw [SignedOrbit.balanced_iff_toNat_eq] at h
  16  constructor
  17  · intro hle
  18    rw [le_iff_toNat_cf] at hle ⊢
  19    omega
  20  · intro hle
  21    rw [le_iff_toNat_cf] at hle ⊢
  22    omega
  23
  24end IndisputableMonolith.PRCGrow.SignedOrbitLeCongrRightOfBalancedChoiceFree
  25

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