proposition: Lemma StepQabsOpp : forall x, StepQabs (-x) == StepQabs (x).
proof: Proof. intros x. unfold StepF_eq. set (g:=(@st_eqS QS)). set (f:=(ap (compose g (compose QabsS QoppS)) QabsS)). cut (StepFfoldProp (f ^@> x)). unfold f. evalStepF. tauto. apply StepFfoldPropForall_Map. intros a. apply: Qabs_opp. 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