proposition: Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
proof: Proof. induction d; try simpl_of_lu; split; trivial; try discriminate; try (intros H; now apply N.eq_add_0 in H). - rewrite N.add_0_l. intros H. apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H. simpl. now rewrite H. - simpl. destruct (nztail d); try discriminate. now destruct IHd as [_ ->]. Qed.
imports: Decimal DecimalFacts PArith NArith