proposition: Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
proof: Proof. induction d; try simpl_of_lu; try easy. rewrite Nat.add_0_l. split; intros H. - apply Nat.eq_mul_0_r in H; auto. rewrite IHd in H. simpl. now rewrite H. - simpl in H. destruct (nztail d); try discriminate. now destruct IHd as [_ ->]. Qed.
imports: Hexadecimal HexadecimalFacts Arith