proposition: Lemma PartitionMeshConcat : forall {R : ConstructiveReals} (a b c : CRcarrier R) (P : @IntervalPartition R a b) (Q : @IntervalPartition R b c), PartitionMesh (ipt_seq (IntervalPartitionConcat P Q)) (S (ipt_last (IntervalPartitionConcat P Q))) == CRmax (PartitionMesh (ipt_seq P) (S (ipt_last P))) (PartitionMesh (ipt_seq Q) (S (ipt_last Q))).
proof: Proof. intro R. assert (forall (xn yn : nat -> CRcarrier R) (p n : nat), xn n == yn O -> PartitionMesh (ConcatSequences xn yn n) (n + p) == CRmax (PartitionMesh xn n) (PartitionMesh yn p)). { induction p. - intros. unfold ConcatSequences. rewrite CRmax_left. 2: apply PartitionMesh_nonneg. rewrite Nat.add_0_r. rewrite (PartitionMesh_ext (fun n0 : nat => if lt_dec n0 n then xn n0 else yn (n0 - n)%nat) xn). reflexivity. intros. destruct (lt_dec n0 n). reflexivity. replace n0 with n. rewrite Nat.sub_diag. symmetry. exact H. apply Nat.le_antisymm. 2: exact H0. apply Nat.nlt_ge. exact n1. - intros. rewrite Nat.add_succ_r. simpl. rewrite IHp. 2: exact H. assert (forall a b c : CRcarrier R, CRmax a (CRmax b c) == CRmax b (CRmax a c)). intros. rewrite CRmax_assoc, (CRmax_sym a), <- CRmax_assoc. reflexivity. setoid_replace (ConcatSequences xn yn n (S (n + p)) - ConcatSequences xn yn n (n+p)) with (yn (S p) - yn p). apply H0. unfold ConcatSequences. destruct (lt_dec (S (n + p)) n). exfalso. apply (proj1 (Nat.lt_nge _ _) l). apply (Nat.le_trans _ (S n + 0)). rewrite Nat.add_0_r. apply le_S, Nat.le_refl. simpl. apply le_n_S, Nat.add_le_mono_l, Nat.le_0_l. clear n0. destruct (lt_dec (n + p) n). exfalso. apply (proj1 (Nat.lt_nge _ _) l). apply (Nat.le_trans _ (n + 0)). rewrite Nat.add_0_r. apply Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l. clear n0. rewrite (Nat.add_comm n), Nat.add_sub. apply CRplus_morph. 2: reflexivity. replace (S (p+n)) with (S p + n)%nat. 2: reflexivity. rewrite Nat.add_sub. reflexivity. } intros. unfold IntervalPartitionConcat, ipt_seq, ipt_last. destruct P, Q. replace (S (S ipt_last0 + ipt_last1)) with (S ipt_last0 + S ipt_last1)%nat. rewrite H. apply CRmax_morph. reflexivity. reflexivity. rewrite <- ipt_lastB0. rewrite <- ipt_head1. reflexivity. rewrite Nat.add_succ_r. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont