proposition: Lemma FSumx_wd' : forall (P : IR -> CProp) n (f g : forall i, i < n -> PartIR), (forall i H H', Feq P (f i H) (g i H')) -> Feq P (FSumx n f) (FSumx n g).
proof: Proof. intros; induction n as [| n Hrecn]. simpl in |- *; apply Feq_reflexive; apply included_IR. simpl in |- *; apply Feq_plus; auto. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality