proposition: Lemma spec_ww_mod_gt_aux : forall ah al bh bl, [[WW ah al]] > [[WW bh bl]] -> 0 < [|bh|] -> [[ww_mod_gt_aux ah al bh bl]] = [[WW ah al]] mod [[WW bh bl]].
proof: Proof. intros. rewrite spec_ww_mod_gt_aux_eq;trivial. assert (H3 := spec_ww_div_gt_aux ah al bl H H0). destruct (ww_div_gt_aux ah al bh bl) as (q,r);simpl. simpl in H,H3. destruct H3;apply Zmod_unique with [[q]]. zarith. rewrite H1;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub