IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeProductRightFactorIffOfBalancedChoiceFree

   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.SignedOrbitLeCongrLeftOfBalancedChoiceFree
   6
   7namespace IndisputableMonolith.PRCGrow.SignedOrbitLeProductRightFactorIffOfBalancedChoiceFree
   8
   9open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  10open IndisputableMonolith.PRCGrow.SignedOrbitLeCongrLeftOfBalancedChoiceFree
  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
  17    rw [← Nat.mul_add, ← Nat.mul_add, hb]
  18  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
  19    rw [← Nat.mul_add, ← Nat.mul_add, hb2]
  20  omega
  21
  22theorem le_product_right_factor_iff_of_balanced_cf {a b b' c : SignedOrbit} (hb : SignedOrbit.balanced b b') : SignedOrbit.le (SignedOrbit.mul a b) c ↔ SignedOrbit.le (SignedOrbit.mul a b') c :=
  23  le_congr_left_of_balanced_cf (mul_balanced_congr_right_cf hb)
  24
  25end IndisputableMonolith.PRCGrow.SignedOrbitLeProductRightFactorIffOfBalancedChoiceFree
  26