proposition: Lemma nztail_to_hex_uint_pow16 n : Hexadecimal.nztail (Pos.to_hex_uint (Nat.iter n (Pos.mul 16) 1%positive)) = (D1 Nil, n).
proof: Proof. case n as [|n]; [now simpl|]. rewrite <-(Nat2Pos.id (S n)); [|now simpl]. generalize (Pos.of_nat (S n)); clear n; intro p. induction (Pos.to_nat p); [now simpl|]. rewrite Unsigned.nat_iter_S. unfold Pos.to_hex_uint. change (Pos.to_little_hex_uint _) with (Unsigned.to_lu (16 * N.pos (Nat.iter n (Pos.mul 16) 1%positive))). rewrite Unsigned.to_lhex_tenfold. revert IHn; unfold Pos.to_hex_uint. unfold Hexadecimal.nztail; rewrite !rev_rev; simpl. set (f'' := _ (Pos.to_little_hex_uint _)). now case f''; intros r n' H; inversion H. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith