fact: Definition square:bigD-> bigD:=fun x:bigD => (dy_mult x x) .
imports: Program QArith ZArith Bignums.BigZ.BigZ Qpossec MetricMorphisms Qmetric Qdlog ARArith MathClasses.implementations.stdlib_rationals MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.fast_integers MathClasses.implementations.dyadics