proposition: Lemma half_spec_even n m : half ((n + n + 1) * 2 ^ (S m)) = ((n + n + 1) * 2 ^ m, true).
proof: Proof. have := half_spec ((n + n + 1) * 2 ^ (S m)). case: (half _) => k []; rewrite /= => ?; congr pair; lia. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun