fact: Definition StepQsrt : (@ring_theory (StepQ) (constStepF (0:QS)) (constStepF (1:QS)) StepQplus StepQmult StepQminus StepQopp (@StepF_eq QS)).
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