proposition: Lemma spec_w_mod_gt_eq : forall a b, [|a|] > [|b|] -> 0 <[|b|] -> [|w_mod_gt a b|] = [|snd (w_div_gt a b)|].
proof: Proof. intros a b Hgt Hpos. rewrite spec_mod_gt;trivial. assert (H:=spec_div_gt Hgt Hpos). destruct (w_div_gt a b) as (q,r);simpl. rewrite Z.mul_comm in H;destruct H. symmetry;apply Zmod_unique with [|q|];trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub