proposition: Lemma of_to (q:IQ) : forall d, to_decimal q = Some d -> of_decimal d = q.
proof: Proof. intro d. case q as [num den|q q'|q q']; simpl. - generalize (of_IQmake_to_decimal' num den). case IQmake_to_decimal' as [d'|]; [|now simpl]. case d' as [i f|]; [|now simpl]. now intros H; injection 1 as <-. - case q as [num den| |]; [|now simpl..]. case q' as [num' den'| |]; [|now simpl..]. case num' as [z p| | |]; [|now simpl..]. case (Z.eq_dec z 10); [intros->|]. 2:{ case z; [now simpl| |now simpl]; intro pz'. case pz'; [intros d0..| ]; [now simpl| |now simpl]. case d0; [intros d1..| ]; [ |now simpl..]. case d1; [intros d2..| ]; [now simpl| |now simpl]. now case d2. } case (Pos.eq_dec den' 1%positive); [intros->|now case den']. generalize (of_IQmake_to_decimal' num den). case IQmake_to_decimal' as [d'|]; [|now simpl]. case d' as [i f|]; [|now simpl]. intros <-; clear num den. injection 1 as <-. unfold of_decimal; simpl. now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. - case q as [num den| |]; [|now simpl..]. case q' as [num' den'| |]; [|now simpl..]. case num' as [z p| | |]; [|now simpl..]. case (Z.eq_dec z 10); [intros->|]. 2:{ case z; [now simpl| |now simpl]; intro pz'. case pz'; [intros d0..| ]; [now simpl| |now simpl]. case d0; [intros d1..| ]; [ |now simpl..]. case d1; [intros d2..| ]; [now simpl| |now simpl]. now case d2. } case (Pos.eq_dec den' 1%positive); [intros->|now case den']. generalize (of_IQmake_to_decimal' num den). case IQmake_to_decimal' as [d'|]; [|now simpl]. case d' as [i f|]; [|now simpl]. intros <-; clear num den. injection 1 as <-. unfold of_decimal; simpl. now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith