proposition: Lemma Rminus_plus_one_lower : forall {R : ConstructiveReals} (a b : CRcarrier R), a <= b -> (a-1) <= (b+1).
proof: Proof. intros. apply (CRle_trans _ a). apply CRlt_asym, Rminus_pos_lower. apply CRzero_lt_one. apply (CRle_trans _ b _ H). apply CRlt_asym, Rplus_pos_higher. apply CRzero_lt_one. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal