no goals
α : Type ?u.860822
m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = toZNum m
cases m <;> constructor <;> intro h <;> try cases h <;> rfl
no goals
case pos.mpr
α : Type ?u.860822
p a✝ : PosNum
h : ZNum.pos p = toZNum (pos a✝)
⊢ pos p = pos a✝
cases h <;> rfl
no goals
α : Type ?u.860822
m : Num
p : PosNum
h : ZNum.neg p = toZNum m
⊢ m ∈ ofZNum' (ZNum.neg p)
cases m <;> cases h