proposition: Lemma to_lu_sixteenfold n : n<>0 -> to_lu (0x10 * n) = D0 (to_lu n).
proof: Proof. induction n. - simpl. now destruct 1. - intros _. destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial. rewrite !Nat.add_succ_r. simpl in *. rewrite (IHn H). now destruct (to_lu n). Qed.
imports: Hexadecimal HexadecimalFacts Arith