proposition: Lemma Q_can_spec : forall q : Q_as_CRing, q [=] Q_can q.
proof: Proof. intro q; destruct q as [qn qd]; unfold Q_can; simpl; unfold Qeq; simpl. rewrite <- Q_can_den_pos_val_spec. unfold Q_can_den, Q_can_num; simpl. assert (Zgcd qn qd <> 0). intro. destruct (Zgcd_zero _ _ H). discriminate. rewrite -> (Zgcd_div_mult_lft qn qd) at 1. rewrite -> (Zgcd_div_mult_rht qn qd) at 6. ring. assumption. assumption. Qed.
imports: CRings Qring Zring Zlcm