proposition: Lemma spec_ww_div : forall a b, 0 < [[b]] -> let (q,r) := ww_div a b in [[a]] = [[q]] * [[b]] + [[r]] /\ 0 <= [[r]] < [[b]].
proof: Proof. intros a b Hpos;unfold ww_div. rewrite spec_ww_compare; case Z.compare_spec; intros. simpl;rewrite spec_ww_1;split;zarith. simpl;split;[ring|Spec_ww_to_Z a;zarith]. apply spec_ww_div_gt;zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub