proposition: Theorem div_gcd_gcd_0_r : ∀ a b c d e f, (b / Z.gcd (Z.gcd a b) c)%Z = (e / Z.gcd (Z.gcd d e) f)%Z → e = 0%Z → (a * e)%Z = (d * b)%Z.
proof: Proof. intros a b c d e f Hb He. subst e. rewrite Z.mul_0_r. rewrite Z.gcd_0_r in Hb. destruct (Z_zerop d) as [Hd| Hd]. subst d; rewrite Z.mul_0_l; reflexivity. rewrite Z.div_0_l in Hb. rewrite Z.gcd_comm, Z.gcd_assoc in Hb. pose proof (Z.gcd_divide_l b (Z.gcd c a)) as H. destruct H as (e, H). rewrite Z.gcd_comm in H. remember (Z.gcd (Z.gcd c a) b) as g. rewrite H in Hb. destruct (Z_zerop g) as [Hg| Hg]. move Hg at top; subst g. rewrite Z.mul_0_r in H; subst b. rewrite Z.mul_0_r; reflexivity. rewrite Z.div_mul in Hb; [ idtac | assumption ]. subst e b. rewrite Z.mul_0_l, Z.mul_0_r; reflexivity. intros H. apply Z.gcd_eq_0_l in H. apply Hd. apply Z.abs_0_iff; assumption. Qed.
imports: Utf8 QArith Sorting ConvexHull ConvexHullMisc Misc NbarM QbarM Newton Field2 Fpolynomial Power_series Puiseux_series Ps_add Ps_add_compat Ps_mul Ps_div