proposition: Lemma dnorm_spec_e d : match d, dnorm d with | Decimal _ _, Decimal _ _ => True | DecimalExp _ _ e, Decimal _ _ => norm e = Pos zero | DecimalExp _ _ e, DecimalExp _ _ e' => e' = norm e /\ e' <> Pos zero | Decimal _ _, DecimalExp _ _ _ => False end.
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