fact: Definition ww_gcd a b := Eval lazy beta delta [ww_gcd_gt] in match ww_compare a b with | Gt => ww_gcd_gt a b | Eq => a | Lt => ww_gcd_gt b a end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub