IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeNeg

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4
   5namespace IndisputableMonolith.PRCGrow.RatioOrbitLeNeg
   6
   7open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   8open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
   9
  10theorem leQ_neg_neg_iff (p q : RatioOrbit) :
  11    leQ (RatioOrbit.negate q) (RatioOrbit.negate p) ↔ leQ p q := by
  12  unfold leQ
  13  rw [SignedOrbit.le_iff_toInt_le, SignedOrbit.le_iff_toInt_le]
  14  simp only [RatioOrbit.negate, SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt,
  15    SignedOrbit.negate_toInt]
  16  constructor
  17  · intro h
  18    have e1 : -(q.num.toInt) * ↑(p.den.toNat) = -(q.num.toInt * ↑(p.den.toNat)) := by ring
  19    have e2 : -(p.num.toInt) * ↑(q.den.toNat) = -(p.num.toInt * ↑(q.den.toNat)) := by ring
  20    rw [e1, e2] at h
  21    omega
  22  · intro h
  23    have e1 : -(q.num.toInt) * ↑(p.den.toNat) = -(q.num.toInt * ↑(p.den.toNat)) := by ring
  24    have e2 : -(p.num.toInt) * ↑(q.den.toNat) = -(p.num.toInt * ↑(q.den.toNat)) := by ring
  25    rw [e1, e2]
  26    omega
  27
  28end IndisputableMonolith.PRCGrow.RatioOrbitLeNeg
  29