proposition: Lemma RL_sum_lemma_aux : forall (n : nat) (P : Partition Hab n) fP (HfP : Points_in_Partition P fP), Partition_Sum HfP incF [=] Fa[*] (b[-]a) [-] Sumx (fun (i : nat) (Hi : i < n) => (Fa[-]Part F (fP i Hi) (just HfP)) [*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))).
proof: Proof. intros; apply eq_transitive_unfolded with (Sumx (fun (i : nat) (Hi : i < n) => Fa[*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))) [-] Sumx (fun (i : nat) (Hi : i < n) => (Fa[-]Part F (fP i Hi) (just HfP)) [*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi)))). eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Sumx_minus_Sumx. unfold Partition_Sum in |- *; apply Sumx_wd; intros. eapply eq_transitive_unfolded. 2: apply ring_distl_minus. apply mult_wdl. rstepr (Part F (fP i H) (just HfP)); algebra. apply cg_minus_wd. 2: algebra. astepr (Fa[*]b[-]Fa[*]a). eapply eq_transitive_unfolded. apply Mengolli_Sum with (f := fun (i : nat) (Hi : i <= n) => Fa[*]P i Hi). red in |- *; intros. apply mult_wdr. apply prf1; auto. intros; algebra. apply cg_minus_wd; apply mult_wdr. apply finish. apply start. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef