proposition: Lemma FSum_comm_scal' : forall (f : nat -> PartIR) c m n x Hx Hx', FSum m n (fun i => [-C-]c{*}f i) x Hx [=] ( [-C-]c{*}FSum m n f) x Hx'.
proof: Proof. intros. simpl in |- *. eapply eq_transitive_unfolded. 2: apply (Sum_comm_scal' (fun n : nat => f n x (ProjIR2 Hx' n)) c m n). apply Sum_wd; intros; rational. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality