proposition: Lemma spec_ww_head00 : forall x, [[x]] = 0 -> [[ww_head0 x]] = Zpos ww_Digits.
proof: Proof. intros x; case x; unfold ww_head0. intros HH; rewrite spec_ww_zdigits; auto. intros xh xl; simpl; intros Hx. case (spec_to_Z xh); intros Hx1 Hx2. case (spec_to_Z xl); intros Hy1 Hy2. assert (F1: [|xh|] = 0). { Z.le_elim Hy1; auto. - absurd (0 < [|xh|] * wB + [|xl|]); auto with zarith. apply Z.lt_le_trans with (1 := Hy1); auto with zarith. pattern [|xl|] at 1; rewrite <- (Z.add_0_l [|xl|]). apply Z.add_le_mono_r; auto with zarith. - Z.le_elim Hx1; auto. absurd (0 < [|xh|] * wB + [|xl|]). auto with zarith. rewrite <- Hy1; rewrite Z.add_0_r. apply Z.mul_pos_pos; auto with zarith. } rewrite spec_compare. case Z.compare_spec. intros H; simpl. rewrite spec_w_add; rewrite spec_w_head00. rewrite spec_zdigits; rewrite spec_ww_digits. rewrite Pos2Z.inj_xO; auto with zarith. rewrite F1 in Hx; auto with zarith. rewrite spec_w_0; auto with zarith. rewrite spec_w_0; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase