proposition: Lemma sum_INR : forall {R : ConstructiveReals} (n:nat), CRsum INR n == INR n * (INR (S n)) * CR_of_Q R (1#2).
proof: Proof. induction n. - unfold CRsum, INR, Z.of_nat. rewrite CRmult_0_l, CRmult_0_l. reflexivity. - transitivity (CRsum INR n + @INR R (S n)). reflexivity. rewrite IHn. clear IHn. transitivity (INR (S n) * (INR n * CR_of_Q R (1#2) + 1)). rewrite CRmult_plus_distr_l. apply CRplus_morph. rewrite <- CRmult_assoc. apply CRmult_morph. 2: reflexivity. apply CRmult_comm. rewrite CRmult_1_r. reflexivity. rewrite CRmult_assoc. apply CRmult_morph. reflexivity. apply (CRmult_eq_reg_r (CR_of_Q R 2)). left. apply CR_of_Q_pos; reflexivity. rewrite CRmult_plus_distr_r, CRmult_1_l. rewrite CRmult_assoc, <- CR_of_Q_mult. rewrite CRmult_assoc, <- (CR_of_Q_mult _ (1#2)). setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. do 2 rewrite CRmult_1_r. rewrite (CR_of_Q_plus R 1 1). do 2 rewrite S_INR. rewrite CRplus_assoc. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal