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