proposition: Lemma WW_0: forall x y, [[WW x y]] = 0 -> [|x|] = 0 /\ [|y|] =0.
proof: Proof. intros x y; simpl; case (ZnZ.spec_to_Z x); intros H1 H2; case (ZnZ.spec_to_Z y); intros H3 H4 H5. case Zle_lt_or_eq with (1 := H1); clear H1; intros H1. absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]). unfold w_to_Z, w_digits in H5;auto with zarith. match goal with |- _ < ?X + _ => apply Z.lt_le_trans with X; auto with zarith end. case Zle_lt_or_eq with (1 := H3); clear H3; intros H3. 2: auto with zarith. absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]). unfold w_to_Z, w_digits in H5; auto with zarith. rewrite <- H1; rewrite Zmult_0_l; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux