Lean4
instance : LinearOrder (ValueGroupWithZero R)
where
le_refl := ValueGroupWithZero.ind fun _ _ => .rfl
le_trans a b c hab
hbc :=
by
induction a using ValueGroupWithZero.ind with
| mk a₁ a₂
induction b using ValueGroupWithZero.ind with
| mk b₁ b₂
induction c using ValueGroupWithZero.ind with
| mk c₁ c₂
rw [ValueGroupWithZero.mk_le_mk] at hab hbc ⊢
apply rel_mul_cancel b₂.prop
calc
a₁ * c₂ * b₂
_ = a₁ * b₂ * c₂ := by rw [mul_right_comm]
_ ≤ᵥ b₁ * a₂ * c₂ := (rel_mul_right (c₂ : R) hab)
_ = b₁ * c₂ * a₂ := by rw [mul_right_comm]
_ ≤ᵥ c₁ * b₂ * a₂ := (rel_mul_right (a₂ : R) hbc)
_ = c₁ * a₂ * b₂ := by rw [mul_right_comm]
le_antisymm a b hab
hba := by
induction a using ValueGroupWithZero.ind
induction b using ValueGroupWithZero.ind
exact ValueGroupWithZero.sound hab hba
le_total a
b := by
induction a using ValueGroupWithZero.ind
induction b using ValueGroupWithZero.ind
rw [ValueGroupWithZero.mk_le_mk, ValueGroupWithZero.mk_le_mk]
apply rel_total
toDecidableLE := Classical.decRel LE.le
