proposition: Lemma AllIntervalsSmallerThanMesh : forall {R : ConstructiveReals} (a b : CRcarrier R) (P : @IntervalPartition R a b) (n : nat), le n (ipt_last P) -> ipt_seq P (S n) - ipt_seq P n <= PartitionMesh (ipt_seq P) (S (ipt_last P)).
proof: Proof. intros. destruct P; unfold ipt_seq, ipt_last; simpl in H. clear ipt_lastB0 b. generalize dependent ipt_last0. induction ipt_last0. - intros. inversion H. apply CRmax_l. - intros. assert (forall n : nat, le n ipt_last0 -> (ipt_seq0 n <= ipt_seq0 (S n))). { intros. apply ipt_ordered0. apply (Nat.le_trans _ ipt_last0 _ H0). apply le_S, Nat.le_refl. } specialize (IHipt_last0 H0). apply Nat.le_succ_r in H. destruct H. + specialize (IHipt_last0 H). apply (CRle_trans _ _ _ IHipt_last0). apply CRmax_r. + rewrite <- H. apply CRmax_l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont