proposition: Lemma spec_ww_mod_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] -> [[ww_mod_gt a b]] = [[a]] mod [[b]].
proof: Proof. intros a b Hgt Hpos. assert (H:= spec_ww_div_gt a b Hgt Hpos). rewrite (spec_ww_mod_gt_eq a b Hgt Hpos). destruct (ww_div_gt a b)as(q,r);destruct H. apply Zmod_unique with[[q]];simpl;trivial. rewrite Z.mul_comm;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub