proposition: Lemma double_nzhead d : double (nzhead d) = nzhead (double d).
proof: Proof. unfold double. rewrite <-!rev_nztail_rev, !rev_rev. apply f_equal; generalize (rev d); clear d; intro d. cut (Little.double (nztail d) = nztail (Little.double d) /\ Little.succ_double (nztail d) = nztail (Little.succ_double d)). { now simpl. } now induction d; [|split; simpl; rewrite <-?(proj1 IHd), <-?(proj2 IHd); case nztail..]. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith