IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitLeMulRightIffOfNonnegFlagOfNotBalancedZeroChoiceFree

   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.OrbitArithmetic
   6import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree
   7
   8namespace IndisputableMonolith.PRCGrow.SignedOrbitLeMulRightIffOfNonnegFlagOfNotBalancedZeroChoiceFree
   9
  10open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  11open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  12
  13theorem cross_le_iff (A B p n : Nat) (hnp : n < p) :
  14    (n * B + p * A ≤ p * B + n * A ↔ A ≤ B) := by
  15  obtain ⟨c, hc⟩ := Nat.exists_eq_add_of_lt hnp
  16  subst hc
  17  have e1 : (n + c + 1) * A = n * A + (c + 1) * A := by ring
  18  have e2 : (n + c + 1) * B = n * B + (c + 1) * B := by ring
  19  rw [e1, e2]
  20  constructor
  21  · intro h
  22    have h2 : (c + 1) * A ≤ (c + 1) * B := by omega
  23    exact Nat.le_of_mul_le_mul_left h2 (Nat.succ_pos c)
  24  · intro h
  25    have h2 : (c + 1) * A ≤ (c + 1) * B := Nat.mul_le_mul (Nat.le_refl _) h
  26    omega
  27
  28theorem le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero_cf :
  29    ∀ (a z w : SignedOrbit), a.nonnegFlag = true →
  30    ¬ a.balanced SignedOrbit.zero →
  31    ((z.mul a).le (w.mul a) ↔ z.le w) := by
  32  intro a z w hanonneg ha
  33  have han : a.neg.toNat ≤ a.pos.toNat := by
  34    have h := hanonneg
  35    unfold SignedOrbit.nonnegFlag at h
  36    rwa [leq_eq_true_iff_cf] at h
  37  have hlt : a.neg.toNat < a.pos.toNat := by
  38    rcases Nat.lt_or_ge a.neg.toNat a.pos.toNat with h | h
  39    · exact h
  40    · exfalso; apply ha
  41      rw [SignedOrbit.balanced_iff_toNat_eq]
  42      rw [show SignedOrbit.zero.neg.toNat = 0 from rfl,
  43          show SignedOrbit.zero.pos.toNat = 0 from rfl]
  44      omega
  45  rw [le_iff_toNat_cf, le_iff_toNat_cf]
  46  have eqL : (w.mul a).neg.toNat + (z.mul a).pos.toNat =
  47      a.neg.toNat * (w.pos.toNat + z.neg.toNat) + a.pos.toNat * (w.neg.toNat + z.pos.toNat) := by
  48    simp only [SignedOrbit.mul_pos, SignedOrbit.mul_neg,
  49              DistinctionNat.toNat_add, DistinctionNat.toNat_mul]
  50    ring
  51  have eqR : (w.mul a).pos.toNat + (z.mul a).neg.toNat =
  52      a.pos.toNat * (w.pos.toNat + z.neg.toNat) + a.neg.toNat * (w.neg.toNat + z.pos.toNat) := by
  53    simp only [SignedOrbit.mul_pos, SignedOrbit.mul_neg,
  54              DistinctionNat.toNat_add, DistinctionNat.toNat_mul]
  55    ring
  56  rw [eqL, eqR]
  57  exact cross_le_iff (w.neg.toNat + z.pos.toNat) (w.pos.toNat + z.neg.toNat)
  58      a.pos.toNat a.neg.toNat hlt
  59
  60end IndisputableMonolith.PRCGrow.SignedOrbitLeMulRightIffOfNonnegFlagOfNotBalancedZeroChoiceFree
  61