proposition: Lemma spec_ww_mod : forall a b, 0 < [[b]] -> [[ww_mod a b]] = [[a]] mod [[b]].
proof: Proof. clear ww_1 spec_ww_1. intros a b Hpos;unfold ww_mod. rewrite spec_ww_compare; case Z.compare_spec; intros. simpl;apply Zmod_unique with 1;try rewrite H;zarith. Spec_ww_to_Z a;symmetry;apply Zmod_small;zarith. apply spec_ww_mod_gt;zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub