proposition: Lemma reverse_sum : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n : nat), CRsum u n == CRsum (fun k => u (n-k)%nat) n.
proof: Proof. induction n. - intros. reflexivity. - rewrite (decomp_sum (fun k : nat => u (S n - k)%nat)). + simpl. rewrite CRplus_comm. apply CRplus_morph. * reflexivity. * assumption. + unfold lt. apply -> Nat.succ_le_mono; apply Nat.le_0_l. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits