proposition: Lemma QreduceApprox_prf : forall (e:Qpos), proj1_sig (Qpos_red e) <= proj1_sig e.
proof: Proof. intros e. destruct e. simpl. rewrite -> Qred_correct. apply Qle_refl. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax