proposition: Lemma PartitionRationalLocSorted : forall {R : ConstructiveReals} (a b : CRcarrier R) (P : @IntervalPartition R a b) (rat : IntervalPartitionRational P), LocallySorted (fun x x0 : QArith_base.Q => is_true (Qle_bool x x0)) (proj1_sig rat).
proof: Proof. intros. apply FunLocSorted. intros. destruct rat; simpl; unfold proj1_sig in H. destruct (Q_dec (nth n x 0) (nth (S n) x 0))%Q. destruct s. apply Qlt_le_weak, q. exfalso. destruct a0. rewrite H0 in H. apply le_S_n, le_S_n in H. apply (CR_of_Q_lt R) in q. rewrite <- H1 in q. rewrite <- (H1 n) in q. destruct P. simpl in q, H1. apply (ipt_ordered0 n). exact H. exact q. apply le_S, H. apply le_n_S, H. rewrite q. apply Qle_refl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont