proposition: Fact fractan_stop_cons_inv p q l x : fractran_stop ((p,q)::l) x <-> ~ divides q (p*x) /\ fractran_stop l x.
proof: Proof. split. * intros H. assert (~ divides q (p*x)) as H'. { intros (z & Hz); apply (H z); constructor; rewrite Hz; ring. } split; auto. intros z Hz; apply (H z); constructor 2; auto. * intros (H1 & H2) z Hz. apply fractran_step_cons_inv in Hz. destruct Hz as [ H3 | (H3 & H4) ]. - apply H1; exists z; rewrite <- H3; ring. - apply (H2 _ H4). Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)