proposition: Lemma κ_mod4 {a b c: nat} : κ (2+a) b c mod 4 = 0.
proof: Proof. apply /div_exact. have -> : κ (2+a) b c = (κ a b c) * 4 by (rewrite /κ /=; lia). by rewrite /κ Nat.div_mul /=; lia. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun