fact: Definition StepQisZero:(StepQ)->bool:=(StepFfold (fun (x:QS) => Qeq_bool x 0) (fun _ x y => x && y)).
imports: CoRN.algebra.RSetoid CoRN.model.metric2.Qmetric Coq.QArith.QArith CoRN.metric2.StepFunctionSetoid Coq.QArith.Qabs Coq.Bool.Bool CoRN.tactics.CornTac CoRN.logic.CornBasics CoRN.algebra.RSetoid