English
DivisibleHull M becomes a strictly ordered module over ℚ≥0, i.e., scalar multiplication by positive rationals respects strict inequality.
Русский
DivisibleHull M становится строго упорядоченным модулем над ℚ≥0: умножение на положительные рациональные числа сохраняет строгий неравенство.
LaTeX
$$IsStrictOrderedModule (\\mathbb{Q}_{\\ge 0}, DivisibleHull M)$$
Lean4
instance : IsOrderedCancelAddMonoid (DivisibleHull M) :=
.of_add_lt_add_left
(fun a b c h ↦
by
induction a with
| mk ma sa
induction b with
| mk mb sb
induction c with
| mk mc sc
simp_rw [mk_add_mk]
rw [mk_lt_mk] at ⊢ h
simp_rw [PNat.mul_coe, mul_smul, smul_add, smul_smul]
have := add_lt_add_left (nsmul_lt_nsmul_right (sa * sa).ne_zero h) ((sa * sb * sc.val) • ma)
simp_rw [PNat.mul_coe, smul_smul] at this
convert this using 3 <;> ring)
