proposition: Lemma κ_pos' {a b c: nat} : κ a b c = 1 + (κ a b c - 1).
proof: Proof. have := @κ_pos _ false true a b c. case: (κ a b c); [done | 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