proposition: Lemma FSumx_wd : forall n (f g : forall i, i < n -> PartIR), (forall i Hi x HxF HxG, f i Hi x HxF [=] g i Hi x HxG) -> forall x HxF HxG, FSumx n f x HxF [=] FSumx n g x HxG.
proof: Proof. intro; case n. intros; simpl in |- *; algebra. clear n. simple induction n. intros; simpl in |- *; algebra. clear n; intro. cut {p : nat | S n = p}; [ intro H | exists (S n); auto ]. elim H; intros p Hp. rewrite Hp; intros. simpl in |- *. apply bin_op_wd_unfolded. apply H0. intros; apply H1. apply H1. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality