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