case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ order (↑C r) = 0

case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : ¬r = 0
⊢ order (↑C r) = 0
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
⊢ order (↑C r) = 0
by_cases h : r = 0
no goals
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ order (↑C r) = 0
rw [h, C_zero, order_zero]
no goals
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : ¬r = 0
⊢ order (↑C r) = 0
exact order_single h