proposition: Lemma Q_can_den_pos_val_spec : forall q : Q_as_CRing, Q_can_den q = Q_can_den_pos_val q.
proof: Proof. intro q; set (Q_can_den_pos q) as z. unfold Q_can_den_pos_val. clearbody z. revert z. case (Q_can_den q). intro; discriminate. reflexivity. intros; discriminate. Qed.
imports: CRings Qring Zring Zlcm