proposition: Fact mma_div_cst_progress a v st : v#>s = a*k -> st = (q,v[0/s][(a+(v#>d))/d]) -> (i, mma_div_cst) // (i,v) -+> st.
proof: Proof. Proof using Hsd Hk. intros H1 H2; subst st; apply mma_div_cst_spec with (1 := H1); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)