proposition: Lemma EquiPartitionRational : forall {R : ConstructiveReals} (a b : Q) (k : nat) (leab : (CR_of_Q R a) <= (CR_of_Q R b)), IntervalPartitionRational (IntervalEquiPartition (CR_of_Q R a) (CR_of_Q R b) k leab).
proof: Proof. intros. exists (Fun2List (fun n => a + (b-a) * (Z.of_nat n # Pos.of_nat (S k)))%Q (2+k)). intros. split. - rewrite Fun2ListLength. reflexivity. - intros. unfold IntervalEquiPartition, ipt_seq. unfold IntervalEquiPartition, ipt_last in H. rewrite Fun2ListNth. 2: apply le_n_S, H. rewrite CR_of_Q_plus. apply CRplus_morph. reflexivity. rewrite CR_of_Q_mult. unfold Qminus. rewrite CR_of_Q_plus, CR_of_Q_opp. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont