proposition: Lemma partition_after_end : forall {R : ConstructiveReals} (a b : CRcarrier R) (P : @IntervalPartition R a b) (n : nat), ipt_seq P n == b -> (forall p:nat, le n p -> le p (S (ipt_last P)) -> ipt_seq P p == b).
proof: Proof. intros. pose proof (ipt_ordered_transit a b P). destruct P; unfold ipt_seq; simpl in H,H1,H2. split. - fold (b <= ipt_seq0 p). rewrite <- H. apply H2. exact H0. exact H1. - fold (ipt_seq0 p <= b). rewrite ipt_lastB0. apply H2. exact H1. apply Nat.le_refl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont