proposition: Lemma of_IQmake_to_decimal' num den : match IQmake_to_decimal' num den with | None => True | Some (DecimalExp _ _ _) => False | Some (Decimal i f) => of_decimal (Decimal i f) = IQmake num den end.
proof: Proof. unfold IQmake_to_decimal'. case_eq (IZ_to_Z num); [intros num' Hnum'|now simpl]. generalize (of_IQmake_to_decimal num' den). case IQmake_to_decimal as [d|]; [|now simpl]. case d as [i f|]; [|now simpl]. now rewrite (IZ_of_Z_IZ_to_Z _ _ Hnum'). Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith