proposition: Lemma StepQRing_Morphism : ring_eq_ext StepQplus StepQmult StepQopp (@StepF_eq QS).
proof: Proof. split. apply: StepQplus_wd. apply: StepQmult_wd. apply: StepQopp_wd. Qed.
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