proposition: Lemma posScale : forall {R : ConstructiveReals} (a : CRcarrier R), 0 < CRmax 1 (CRabs _ a).
proof: Proof. intros. apply (CRlt_le_trans 0 1). apply CRzero_lt_one. apply CRmax_l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal