proposition: Fact fractan_stop_nil_inv x : fractran_stop nil x <-> True.
proof: Proof. split; try tauto; intros _ z; rewrite fractran_step_nil_inv; tauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)