proposition: Lemma in_refinement_packet : forall {R : ConstructiveReals} (a b : CRcarrier R) (n i : nat) (x y : nat -> CRcarrier R) (P Q : @IntervalPartition R a b) (subseq : nat -> nat), WeavedLists x (ipt_seq P) (ipt_last P) -> WeavedLists y (ipt_seq Q) (ipt_last Q) -> IntervalPartitionRefinement _ _ P Q subseq -> le n (ipt_last P) -> le (subseq n) i -> lt i (subseq (S n)) -> CRabs _ (x n - y i) <= PartitionMesh (ipt_seq P) (S (ipt_last P)).
proof: Proof. intros. assert (ipt_seq P n <= y i /\ y i <= ipt_seq P (S n)). { specialize (H0 i). split. apply (CRle_trans _ (ipt_seq Q i)). apply (CRle_trans _ (ipt_seq Q (subseq n))). destruct H1. rewrite H1. apply CRle_refl. apply (Nat.le_trans _ _ _ H2). apply le_S, Nat.le_refl. apply ipt_ordered_transit. exact H3. destruct H1. apply (Nat.le_trans _ (subseq (S n))). apply (Nat.le_trans _ (S i)). apply le_S, Nat.le_refl. exact H4. apply H5. apply le_n_S. exact H2. apply H0. destruct H1. apply le_S_n. apply (Nat.le_trans _ _ _ H4). apply H5, le_n_S, H2. apply (CRle_trans _ (ipt_seq Q (S i))). apply H0. apply le_S_n. apply (Nat.le_trans _ _ _ H4). destruct H1. apply H5, le_n_S, H2. destruct H1. apply (CRle_trans _ (ipt_seq Q (subseq (S n)))). apply ipt_ordered_transit. exact H4. apply H5, le_n_S, H2. rewrite H1. apply CRle_refl. apply le_n_S, H2. } apply (CRle_trans _ (ipt_seq P (S n) - ipt_seq P n)). apply Rsmaller_interval. apply H5. apply H5. apply H. exact H2. apply H. exact H2. apply AllIntervalsSmallerThanMesh. exact H2. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont