proposition: Lemma dnorm_spec_f d : let f := match d with Decimal _ f => f | DecimalExp _ f _ => f end in let f' := match dnorm d with Decimal _ f => f | DecimalExp _ f _ => f end in f' = f.
proof: Proof. case d as [i f|i f e]; [now simpl|]. simpl; case (int_eq_dec (norm e) (Pos zero)); [now intros->|intro He]. set (i' := match i with Pos _ => _ | _ => _ end). set (m := match norm e with Pos Nil => _ | _ => _ end). replace m with (DecimalExp i' f (norm e)); [now simpl|]. unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl]. now case e; clear e; [|intro e; case e|..]. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith