proposition: Lemma pos_K : K = 1 + (K - 1).
proof: Proof. Proof using HK. suff: K <> 0 by lia. move=> H'K. have := HK (0, (0, 0)). rewrite H'K. move=> [[|L]]. - move=> [_]. apply. apply: rt_refl. - move=> ? /=. lia. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties ConstructiveEpsilon Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Deciders.MM2_UBOUNDED_dec Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun