simp [cong2, FinInt.sub_toUint, FinInt.add_toUint]
case a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint (C - (X + C2)) ≡ toUint (C - C2 - X) [2^sz]
case a
sz : ℕ
C X C2 : FinInt sz
⊢ mod2 (toUint C - (toUint X + toUint C2)) sz = mod2 (toUint C - toUint C2 - toUint X) sz