fact: Variable spec_ww_div_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] -> let (q,r) := ww_div_gt a b in [[a]] = [[q]] * [[b]] + [[r]] /\ 0 <= [[r]] < [[b]].
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub