proposition: Lemma PartitionRationalConcat : forall {R : ConstructiveReals} (a b c : CRcarrier R) (P : @IntervalPartition R a b) (Q : @IntervalPartition R b c), IntervalPartitionRational P -> IntervalPartitionRational Q -> IntervalPartitionRational (IntervalPartitionConcat P Q).
proof: Proof. intros. destruct H, a0, H0, a0. exists (x ++ tl x0). intros. destruct P, Q; simpl; simpl in H, H2, H1, H0. split. - rewrite app_length, H. destruct x0. exfalso; inversion H0. simpl. simpl in H0. inversion H0. rewrite H4. rewrite Nat.add_succ_r. reflexivity. - intros. unfold ConcatSequences. destruct (lt_dec n (S ipt_last0)). + rewrite app_nth1. apply H1. apply le_S_n in l. apply (Nat.le_trans _ ipt_last0 _ l), le_S, Nat.le_refl. rewrite H. apply (Nat.lt_trans _ _ _ l), Nat.le_refl. + destruct (Nat.lt_trichotomy n (S ipt_last0)). contradiction. destruct H4. subst n. rewrite app_nth1. rewrite Nat.sub_diag, <- ipt_head1. rewrite <- H1. rewrite <- ipt_lastB0. reflexivity. apply Nat.le_refl. rewrite H. apply Nat.le_refl. clear n0. rewrite app_nth2, H. 2: rewrite H; exact H4. destruct x0. exfalso; inversion H0. simpl. specialize (H2 (S(n - S (S(ipt_last0))))%nat). simpl in H2. rewrite <- H2. replace (n - S ipt_last0)%nat with (S (n - S (S ipt_last0))). reflexivity. rewrite (Nat.sub_succ_r _ (S ipt_last0)). rewrite Nat.succ_pred. reflexivity. intro abs. apply Nat.sub_0_le in abs. exact (proj1 (Nat.lt_nge _ _) H4 abs). rewrite (Nat.sub_succ_r _ (S ipt_last0)). rewrite Nat.succ_pred. rewrite Nat.le_sub_le_add_l, Nat.add_succ_r. exact H3. intro abs. apply Nat.sub_0_le in abs. exact (proj1 (Nat.lt_nge _ _) H4 abs). Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont