proposition: Lemma κ_21 {a b c: nat} : κ a b c * 2 / 1 = κ (1+a) b c.
proof: Proof. rewrite /κ /= Nat.div_1_r. by 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