proposition: Lemma qs_exp i n u (v : vec nat n) : divides (qs u) (encode_state (i,v)) <-> divides (qs u) (exp 0 v).
proof: Proof. split. - intros [ | ] % divides_mult_inv; eauto. now eapply qs_ps_div in H. - intros. unfold encode_state. now eapply divides_mult. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs mm_no_self) Undecidability.FRACTRAN(FRACTRAN fractran_utils prime_seq FRACTRAN_sss)