proposition: Lemma of_lu_succ d : of_lu (Little.succ d) = S (of_lu d).
proof: Proof. induction d; trivial. simpl_of_lu. rewrite IHd. simpl_of_lu. now rewrite Nat.mul_succ_r, <- (Nat.add_comm 0x10). Qed.
imports: Hexadecimal HexadecimalFacts Arith