fact: Fixpoint FSumx (n : nat) : (forall i, i < n -> PartIR) -> PartIR := match n return ((forall i, i < n -> PartIR) -> PartIR) with | O => fun _ => [-C-][0] | S p => fun f => FSumx p (fun i l => f i (Nat.lt_lt_succ_r i p l)) {+} f p (Nat.lt_succ_diag_r p) end.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality