`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeCongrLeftOfBalancedChoiceFree`

IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/SignedOrbitLeCongrLeftOfBalancedChoiceFree.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.SignedOrbitLeCongrLeftOfBalancedChoiceFree
   8
   9open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  10open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  11
  12theorem le_congr_left_of_balanced_cf {a a' b : SignedOrbit}
  13    (h : SignedOrbit.balanced a a') :
  14    SignedOrbit.le a b ↔ SignedOrbit.le a' 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.SignedOrbitLeCongrLeftOfBalancedChoiceFree
  25

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