proposition: Lemma fractran_step_zero l : Forall (fun c => fst c <> 0) l -> forall x y, x <> 0 -> l /F/ x ≻ y <-> remove_zero_den l /F/ x ≻ y.
proof: Proof. induction 1 as [ | (p,q) l H1 H2 IH2 ]; intros x y Hxy; simpl in *. * split; simpl; inversion 1. * simpl; destruct (eq_nat_dec q 0) as [ Hq | Hq ]. - rewrite <- IH2; auto; subst; split; intros H. + apply fractran_step_cons_inv in H; destruct H as [ H | (H3 & H4) ]; auto. simpl in H; symmetry in H; apply Nat.eq_mul_0 in H; lia. + constructor 2; auto; intros H'. apply divides_0_inv, Nat.eq_mul_0 in H'; lia. - split; intros H. + apply fractran_step_cons_inv in H; destruct H as [ H | (H3 & H4) ]; auto. -- constructor 1; auto. -- constructor 2; auto; apply IH2; auto. + apply fractran_step_cons_inv in H; destruct H as [ H | (H3 & H4) ]; auto. -- constructor 1; auto. -- constructor 2; auto; apply IH2; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)