IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitNonnegFlagMulOfOrbitRightOfNeZeroChoiceFree

   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.SignedOrbitNonnegFlagMulOfOrbitRightOfNeZeroChoiceFree
   8
   9open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  10open IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  11
  12theorem nonnegFlag_mul_ofOrbit_right_of_ne_zero_cf
  13    (z : SignedOrbit) (d : DistinctionNat) (hd : d ≠ DistinctionNat.zero) :
  14    (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).nonnegFlag = z.nonnegFlag := by
  15  have hd' : d.toNat ≠ 0 := by
  16    intro h
  17    apply hd
  18    rw [← DistinctionNat.ofNat_toNat d, h, DistinctionNat.ofNat_zero]
  19  have hdpos : 0 < d.toNat := by omega
  20  have hpos : (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos.toNat = z.pos.toNat * d.toNat := by
  21    show (z.pos * (SignedOrbit.ofOrbit d).pos + z.neg * (SignedOrbit.ofOrbit d).neg).toNat = _
  22    have hp : (SignedOrbit.ofOrbit d).pos = d := rfl
  23    have hn : (SignedOrbit.ofOrbit d).neg = DistinctionNat.zero := rfl
  24    rw [hp, hn, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul,
  25      DistinctionNat.toNat_zero]
  26    omega
  27  have hneg : (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg.toNat = z.neg.toNat * d.toNat := by
  28    show (z.pos * (SignedOrbit.ofOrbit d).neg + z.neg * (SignedOrbit.ofOrbit d).pos).toNat = _
  29    have hp : (SignedOrbit.ofOrbit d).pos = d := rfl
  30    have hn : (SignedOrbit.ofOrbit d).neg = DistinctionNat.zero := rfl
  31    rw [hp, hn, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul,
  32      DistinctionNat.toNat_zero]
  33    omega
  34  have key : DistinctionNat.leq (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg
  35      (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos = true ↔
  36      DistinctionNat.leq z.neg z.pos = true := by
  37    rw [leq_eq_true_iff_cf, leq_eq_true_iff_cf, hpos, hneg]
  38    constructor
  39    · intro h
  40      exact Nat.le_of_mul_le_mul_right h hdpos
  41    · intro h
  42      exact Nat.mul_le_mul_right _ h
  43  show DistinctionNat.leq (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg
  44      (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos =
  45      DistinctionNat.leq z.neg z.pos
  46  cases hb : DistinctionNat.leq z.neg z.pos with
  47    | true => exact key.mpr hb
  48    | false =>
  49      cases hb2 : DistinctionNat.leq (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg
  50          (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos with
  51        | true =>
  52          rw [key.mp hb2] at hb
  53          exact absurd hb (by decide)
  54        | false => rfl
  55
  56end IndisputableMonolith.PRCGrow.SignedOrbitNonnegFlagMulOfOrbitRightOfNeZeroChoiceFree
  57