fact: Definition mul_add:= w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleAdd DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv CyclicAxioms