proposition: Lemma of_IQmake_to_hexadecimal num den : match IQmake_to_hexadecimal num den with | None => True | Some (HexadecimalExp _ _ _) => False | Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IRQ (QArith_base.Qmake num den) end.
proof: Proof. unfold IQmake_to_hexadecimal. case (Pos.eq_dec den 1); [now intros->|intro Hden]. assert (Hf : match QArith_base.IQmake_to_hexadecimal num den with | Some (Hexadecimal i f) => f <> Nil | _ => True end). { unfold QArith_base.IQmake_to_hexadecimal; simpl. generalize (Unsigned.nztail_to_hex_uint den). case Hexadecimal.nztail as [den' e_den']. case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'. case den'; [ |now simpl..]; clear den'. case e_den' as [|e_den']; [now simpl; intros H _; apply Hden; injection H|]. intros _. case Nat.ltb_spec; intro He_den'. - apply del_head_nonnil. revert He_den'; case nb_digits as [|n]; [now simpl|]. now intro H; simpl; apply Nat.lt_succ_r, Nat.le_sub_l. - apply nb_digits_n0. now rewrite nb_digits_iter_D0, Nat.sub_add. } replace (match den with 1%positive => _ | _ => _ end) with (QArith_base.IQmake_to_hexadecimal num den); [|now revert Hden; case den]. generalize (of_IQmake_to_hexadecimal num den). case QArith_base.IQmake_to_hexadecimal as [d'|]; [|now simpl]. case d' as [i f|]; [|now simpl]. unfold of_hexadecimal; simpl. injection 1 as H <-. generalize (f_equal QArith_base.IZ_to_Z H); clear H. rewrite !IZ_to_Z_IZ_of_Z; injection 1 as <-. now revert Hf; case f. Qed.
imports: Decimal DecimalFacts Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ HexadecimalQ Rdefinitions