proposition: Lemma κ_54 {a b c: nat} : κ (2+a) b c * 5 / 4 = κ a b (1+c).
proof: Proof. have -> : κ (2+a) b c * 5 = (5 * κ 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