α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : CPRankMax1 x
h' : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : CPRankMax1 x
⊢ CPRankMax 1 x
have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero
no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : CPRankMax1 x
h' : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x
rwa [zero_add, add_zero] at h'