proposition: Lemma double_unorm d : double (unorm d) = unorm (double d).
proof: Proof. unfold double. rewrite <-!rev_lnorm_rev, !rev_rev, <-!to_of_lu, of_lu_double. now case of_lu; [now simpl|]; intro p; induction p. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith