Require Import Coq.QArith.QArith.
(**
  Abbreviations for construction proper rational numbers from injected natural numbers
**)
Definition negativePower base exp :Q := 1 # base^exp.

Definition rationalFromNum n unitsBehindColon exp :Q :=
  (n * (negativePower (10) unitsBehindColon) * (negativePower (2) exp))%Q.