proposition: Lemma CommonRationalRefinement : forall {R : ConstructiveReals} (a b : CRcarrier R) (P Q : @IntervalPartition R a b), IntervalPartitionRational P -> IntervalPartitionRational Q -> @CommonChaslesRefinement R a b P Q.
proof: Proof. intros. exists (fun n => MergeInjectL (proj1_sig H) (proj1_sig H0) n), (fun n => MergeInjectR (proj1_sig H) (proj1_sig H0) n), (RationalPartitionMerge a b P Q H H0). split. - destruct H,H0; unfold proj1_sig. split. 2: split. + intros. unfold RationalPartitionMerge, ipt_seq; unfold proj1_sig. destruct P,Q; simpl in a0; unfold ipt_last in H; unfold ipt_last; unfold ipt_last, ipt_seq in a1. destruct a0, a1. rewrite H1. 2: exact H. apply CR_of_Q_morph. rewrite (MergeInjectLSpec (S (2 + ipt_last0 + (2+ ipt_last1)))). reflexivity. rewrite H0, H2. apply Nat.le_refl. rewrite H0. apply le_n_S, H. + apply ordered_transit. intros. destruct a0, a1. apply (MergeInjectLInc (S (2 + ipt_last P + (2+ ipt_last Q)))). rewrite H0, H2. apply Nat.le_refl. rewrite H0. apply le_n_S, H. + unfold RationalPartitionMerge, ipt_last. destruct P,Q; simpl in a0, a1. intros. destruct a0, a1. apply le_S_n. apply (Nat.le_trans _ (S (S ipt_last0) + S (S ipt_last1))). rewrite <- H0, <- H2. apply (MergeInjectLBound (S (2 + ipt_last0 + (2+ ipt_last1)))). rewrite H0, H2. apply Nat.le_refl. rewrite H0. apply le_n_S, H. simpl. do 2 rewrite Nat.add_succ_r. apply Nat.le_refl. - destruct H,H0; unfold proj1_sig. split. 2: split. + intros. unfold RationalPartitionMerge, ipt_seq; unfold proj1_sig. destruct P,Q; simpl in a0; unfold ipt_last in H; unfold ipt_last; unfold ipt_last, ipt_seq in a1. destruct a0, a1. rewrite H3. 2: exact H. apply CR_of_Q_morph. rewrite (MergeInjectRSpec (S (2 + ipt_last0 + (2+ ipt_last1)))). reflexivity. rewrite H0, H2. apply Nat.le_refl. rewrite H2. apply le_n_S, H. + apply ordered_transit. intros. destruct a0, a1. apply (MergeInjectRInc (S (2 + ipt_last P + (2+ ipt_last Q)))). rewrite H0, H2. apply Nat.le_refl. rewrite H2. apply le_n_S, H. + unfold RationalPartitionMerge, ipt_last. destruct P,Q; simpl in a0, a1. intros. destruct a0, a1. apply le_S_n. apply (Nat.le_trans _ (S (S ipt_last0) + S (S ipt_last1))). rewrite <- H0, <- H2. apply (MergeInjectRBound (S (2 + ipt_last0 + (2+ ipt_last1)))). rewrite H0, H2. apply Nat.le_refl. rewrite H2. apply le_n_S, H. simpl. do 2 rewrite Nat.add_succ_r. apply Nat.le_refl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont