proposition: Lemma spec_ww_is_zero: forall x, if ww_is_zero x then [[x]] = 0 else 0 < [[x]].
proof: Proof. intro x; unfold ww_is_zero. rewrite spec_ww_compare. case Z.compare_spec. 1-2: zarith. simpl ww_to_Z. assert (V4 := spec_ww_to_Z w_digits w_to_Z spec_to_Z x);zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase