proposition: Lemma doubleSpeed_prf : forall (e:Qpos), proj1_sig ((1#2) * e)%Qpos <= proj1_sig e.
proof: Proof. intros e. autorewrite with QposElim. rewrite -> Qle_minus_iff. simpl. ring_simplify. apply (Qle_trans _ ((1#2) * 0)). rewrite Qmult_0_r. apply Qle_refl. apply Qmult_le_l. reflexivity. destruct e. apply Qlt_le_weak, q. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax