proposition: Theorem div_gcd_gcd_mul_compat : ∀ a b c d e f, (a / Z.gcd (Z.gcd a b) c)%Z = (d / Z.gcd (Z.gcd d e) f)%Z → (b / Z.gcd (Z.gcd a b) c)%Z = (e / Z.gcd (Z.gcd d e) f)%Z → (a * e)%Z = (d * b)%Z.
proof: Proof. intros a b c d e f Ha Hb. destruct (Z_zerop e) as [He| He]. eapply div_gcd_gcd_0_r; eassumption. destruct (Z_zerop d) as [Hd| Hd]. rewrite Z.mul_comm; symmetry. rewrite Z.mul_comm; symmetry. symmetry. apply div_gcd_gcd_0_r with (c := c) (f := f); [ idtac | assumption ]. replace (Z.gcd b a) with (Z.gcd a b) by apply Z.gcd_comm. replace (Z.gcd e d) with (Z.gcd d e) by apply Z.gcd_comm. assumption. apply Z.mul_cancel_r with (p := e) in Ha; [ idtac | assumption ]. rewrite Z_div_mul_swap in Ha. rewrite Z_div_mul_swap in Ha. apply Z.mul_cancel_l with (p := d) in Hb; [ idtac | assumption ]. rewrite Z.mul_comm in Hb. rewrite Z_div_mul_swap in Hb. symmetry in Hb. rewrite Z.mul_comm in Hb. rewrite Z_div_mul_swap in Hb. rewrite Z.mul_comm in Hb. rewrite Hb in Ha. apply Z_div_reg_r in Ha. rewrite Ha; apply Z.mul_comm. apply Z.divide_mul_l. rewrite <- Z.gcd_assoc. apply Z.gcd_divide_l. apply Z.divide_mul_l. rewrite Z.gcd_comm, Z.gcd_assoc. apply Z.gcd_divide_r. rewrite Z.gcd_comm, Z.gcd_assoc. apply Z.gcd_divide_r. rewrite Z.gcd_comm, Z.gcd_assoc. apply Z.gcd_divide_r. rewrite <- Z.gcd_assoc. apply Z.gcd_divide_l. rewrite <- Z.gcd_assoc. apply Z.gcd_divide_l. 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