proposition: Lemma rel_prime_cross_prod : forall a b c d:Z, rel_prime a b -> rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d.
proof: Proof. intros a b c d; intros H H0 H1 H2 H3. elim (Z.divide_antisym b d). - intros H4; split; auto with zarith. rewrite H4 in H3. rewrite Z.mul_comm in H3. apply Z.mul_reg_l with d; auto. contradict H2; rewrite H2; discriminate. - intros H4; contradict H1; rewrite H4. apply Zgt_asym, Z.lt_gt, Z.opp_lt_mono. now rewrite Z.opp_involutive; apply Z.gt_lt. - apply Gauss with a. + rewrite H3; auto with zarith. + now apply Zis_gcd_sym. - apply Gauss with c. + rewrite Z.mul_comm. rewrite <- H3. auto with zarith. + now apply Zis_gcd_sym. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat