proposition: Lemma to_of_lu_sixteenfold d : to_lu (of_lu d) = lnorm d -> to_lu (0x10 * of_lu d) = lnorm (D0 d).
proof: Proof. intro IH. destruct (Nat.eq_dec (of_lu d) 0) as [H|H]. - rewrite H. simpl. rewrite of_lu_0 in H. unfold lnorm. simpl. now rewrite H. - rewrite (to_lu_sixteenfold _ H), IH. rewrite of_lu_0 in H. unfold lnorm. simpl. now destruct (nztail d). Qed.
imports: Hexadecimal HexadecimalFacts Arith