proposition: Lemma of_hex_int_iter_D0 d n : Z.of_hex_int (app_int d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 0x10) (Z.of_hex_int d).
proof: Proof. case d; clear d; intro d; simpl. - now rewrite of_hex_uint_iter_D0. - rewrite of_hex_uint_iter_D0; induction n; [now simpl|]. rewrite !Unsigned.nat_iter_S, <-IHn; ring. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith