proposition: Lemma double_norm d : double (norm d) = norm (double d).
proof: Proof. destruct d. - now simpl; rewrite Unsigned.double_unorm. - simpl; rewrite <-Unsigned.double_nzhead. case (uint_eq_dec (nzhead d) Nil); intro Hnzd. + now rewrite Hnzd. + assert (H : Unsigned.double (nzhead d) <> Nil). { unfold Unsigned.double. intro H; apply Hnzd, rev_nil_inv. now generalize (rev_nil_inv _ H); case rev. } revert H. set (r := Unsigned.double _). set (m := match r with Nil => Pos zero | _ => _ end). intro H. assert (H' : m = Neg r). { now unfold m; clear m; revert H; case r. } rewrite H'; unfold r; clear m r H H'. now revert Hnzd; case nzhead. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith