proposition: Lemma Q_can_spec2 : forall q : Q_as_CRing, Zrelprime (Qnum (Q_can q)) (Qden (Q_can q)).
proof: Proof. intro q; destruct q as [qn qd]. unfold Q_can; simpl. rewrite <- Q_can_den_pos_val_spec. unfold Q_can_den, Q_can_num; simpl. apply Zgcd_div_gcd_1. intro. destruct (Zgcd_zero _ _ H). discriminate. Qed.
imports: CRings Qring Zring Zlcm