proposition: Lemma κ_pos {X: Type} {x y: X} {a b c: nat} : match κ a b c with | 0 => x | S _ => y end = y.
proof: Proof. rewrite /κ. have ? := Nat.pow_nonzero 2 a ltac:(lia). have ? := Nat.pow_nonzero 3 b ltac:(lia). have ? := Nat.pow_nonzero 5 c ltac:(lia). by have -> : let n := 2 ^ a * 3 ^ b * 5 ^ c in n = S (n - 1) by nia. 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