R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type ?u.19931
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.20013
inst✝¹ : DecidableEq ι
x y z v : M
r : R
h✝ : 0 ≤ r
h : 0 < r
inst✝ : Nontrivial R
⊢ 0 < 1
R : Type u_1
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.19931
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type ?u.20013
inst✝ : DecidableEq ι
x y z v : M
r : R
h✝ : 0 ≤ r
h : 0 < r
⊢ 0 < 1
nontriviality R
no goals
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type ?u.19931
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.20013
inst✝¹ : DecidableEq ι
x y z v : M
r : R
h✝ : 0 ≤ r
h : 0 < r
inst✝ : Nontrivial R
⊢ 0 < 1
exact zero_lt_one