proposition: Lemma to_decimal_inj q q' : to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'.
proof: Proof. intros Hnone EQ. generalize (of_to q) (of_to q'). rewrite <-EQ. revert Hnone; case to_decimal; [|now simpl]. now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith