proposition: Lemma dnorm_spec_e d : match d, dnorm d with | Hexadecimal _ _, Hexadecimal _ _ => True | HexadecimalExp _ _ e, Hexadecimal _ _ => Decimal.norm e = Decimal.Pos Decimal.zero | HexadecimalExp _ _ e, HexadecimalExp _ _ e' => e' = Decimal.norm e /\ e' <> Decimal.Pos Decimal.zero | Hexadecimal _ _, HexadecimalExp _ _ _ => False end.
proof: Proof. case d as [i f|i f e]; [now simpl|]. simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); [now intros->|intro He]. set (i' := match i with Pos _ => _ | _ => _ end). set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). replace m with (HexadecimalExp i' f (Decimal.norm e)); [now simpl|]. unfold m; revert He; case (Decimal.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 Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith