proposition: Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y*(x/y) = x.
proof: Proof. unfold Qcdiv. intros. rewrite Qcmult_assoc. rewrite Qcmult_comm. rewrite Qcmult_assoc. rewrite Qcmult_inv_l; auto. apply Qcmult_1_l. Qed.
imports: Field QArith Znumtheory Eqdep_dec