fact: Definition CReal_mult_seq (x y : CReal) := (fun n : Z => seq x (n - scale y - 1)%Z * seq y (n - scale x - 1)%Z).
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra