IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLtTrichotomy

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder
   3import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitLeReflTotal
   4
   5namespace IndisputableMonolith.PRCGrow.RatioOrbitLtTrichotomy
   6
   7open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
   8open IndisputableMonolith.PRCGrow.RatioOrbitLeReflTotal
   9
  10def ltQ (p q : RatioOrbit) : Prop := leQ p q ∧ ¬ RatioOrbit.crossEq p q
  11
  12theorem ltQ_irrefl (p : RatioOrbit) : ¬ ltQ p p := by
  13  intro h
  14  exact h.2 (RatioOrbit.crossEq_refl p)
  15
  16instance crossEq_decidable (a b : RatioOrbit) : Decidable (RatioOrbit.crossEq a b) := by
  17  unfold RatioOrbit.crossEq
  18  infer_instance
  19
  20theorem ltQ_trichotomy (p q : RatioOrbit) :
  21    ltQ p q ∨ RatioOrbit.crossEq p q ∨ ltQ q p := by
  22  cases' leQ_total p q with hpq hqp
  23  · by_cases heq : RatioOrbit.crossEq p q
  24    · exact Or.inr (Or.inl heq)
  25    · exact Or.inl ⟨hpq, heq⟩
  26  · by_cases heq : RatioOrbit.crossEq q p
  27    · exact Or.inr (Or.inl (RatioOrbit.crossEq_symm heq))
  28    · exact Or.inr (Or.inr ⟨hqp, heq⟩)
  29
  30end IndisputableMonolith.PRCGrow.RatioOrbitLtTrichotomy
  31