match H: sz with
| 0 => decide
| sz'+1 =>
    have h: sz' + 1 > 0 := by sorry_arith
    apply eq_of_toUint_cong2
    simp [toUint_minusOne]
    simp [neg_toUint]
    apply cong2_mod2_left
    simp [ofInt_1, toUint_one h]
    sorry_arith
sz : ℕ
⊢ -1 = minusOne
no goals