proposition: Lemma StepF_Sth (X : RSetoid) : (Setoid_Theory (StepF X) (@StepF_eq X)).
proof: Proof. split; unfold Reflexive, Symmetric, Transitive; eauto with sfarith. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunction CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields