rw [PNat.mk_coe] at hc
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b