proposition: Lemma StepQ_le_refl:forall x, (x <= x).
proof: Proof. intros x. unfold StepQ_le. cut (StepFfoldProp (join QleS ^@> x)). evalStepF. tauto. apply StepFfoldPropForall_Map. intros. simpl. auto with *. 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