proposition: Lemma ipt_ordered_transit : forall {R : ConstructiveReals} (a b : CRcarrier R) (P : @IntervalPartition R a b) (n p : nat), le n p -> le p (S (ipt_last P)) -> ipt_seq P n <= ipt_seq P p.
proof: Proof. induction p. - intros. inversion H. apply CRle_refl. - intros. apply Nat.le_succ_r in H. destruct H. + apply (CRle_trans _ (ipt_seq P p)). apply (IHp H). apply (Nat.le_trans _ (ipt_last P)). apply le_S_n. exact H0. apply le_S, Nat.le_refl. apply P. apply le_S_n. exact H0. + subst n. apply CRle_refl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont