proposition: Lemma den_1_div_iff : forall q : Q_as_CRing, Q_can_den q = 1 <-> Zdivides (Qden q) (Qnum q).
proof: Proof. intro q. split; intro H. unfold Q_can_den in H. destruct q; simpl in *. cut (Zpos Qden = Zgcd Qnum Qden). intro H0; rewrite H0. apply Zgcd_is_divisor_lft. rewrite (Zgcd_div_mult_rht Qnum Qden) at 1. rewrite H. apply Zmult_1_l. intro. destruct (Zgcd_zero _ _ H0). rewrite H1 in H. rewrite H2 in H. rewrite Zgcd_zero_rht in H. rewrite Zdiv_0_r in H. discriminate. unfold Q_can_den. destruct q; simpl in *. case (Z_dec Qnum 0). intro H0; rewrite H0. rewrite Zgcd_zero_lft. apply Z_div_same_full. discriminate. intro Hap. cut (Zpos Qden = Zgcd Qnum Qden). intro H0; rewrite H0 at 1. apply Z_div_same_full. intro H1; destruct (Zgcd_zero _ _ H1). discriminate. symmetry. apply Zgcd_divisor; assumption. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg