IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeOfProductRightFactorIffOfBalancedChoiceFree

   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.SignedOrbitLeCongrRightOfBalancedChoiceFree
   6
   7namespace IndisputableMonolith.PRCGrow.SignedOrbitLeOfProductRightFactorIffOfBalancedChoiceFree
   8
   9open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  10open IndisputableMonolith.PRCGrow.SignedOrbitLeCongrRightOfBalancedChoiceFree
  11
  12theorem mul_balanced_congr_right_cf {a b b' : SignedOrbit} (hb : SignedOrbit.balanced b b') : SignedOrbit.balanced (SignedOrbit.mul a b) (SignedOrbit.mul a b') := by
  13  rw [SignedOrbit.balanced_iff_toNat_eq] at hb ⊢
  14  simp only [SignedOrbit.mul_pos, SignedOrbit.mul_neg, DistinctionNat.toNat_add, DistinctionNat.toNat_mul]
  15  have hb2 : b.neg.toNat + b'.pos.toNat = b'.neg.toNat + b.pos.toNat := by omega
  16  have e1 : a.pos.toNat * b.pos.toNat + a.pos.toNat * b'.neg.toNat = a.pos.toNat * b'.pos.toNat + a.pos.toNat * b.neg.toNat := by rw [← Nat.mul_add, ← Nat.mul_add, hb]
  17  have e2 : a.neg.toNat * b.neg.toNat + a.neg.toNat * b'.pos.toNat = a.neg.toNat * b'.neg.toNat + a.neg.toNat * b.pos.toNat := by rw [← Nat.mul_add, ← Nat.mul_add, hb2]
  18  omega
  19
  20theorem le_of_product_right_factor_iff_of_balanced_cf {c a b b' : SignedOrbit} (hb : SignedOrbit.balanced b b') : SignedOrbit.le c (SignedOrbit.mul a b) ↔ SignedOrbit.le c (SignedOrbit.mul a b') :=
  21  le_congr_right_of_balanced_cf (mul_balanced_congr_right_cf hb)
  22
  23end IndisputableMonolith.PRCGrow.SignedOrbitLeOfProductRightFactorIffOfBalancedChoiceFree
  24