proposition: Lemma ref_calc4 : AbsIR (Sumx (fun (i : nat) (Hi : i < n) => Sum2 (fun (j : nat) (Hj : sub i <= j) (Hj' : j <= pred (sub (S i))) => Part F (fP i Hi) just1[*] (Q _ (H' _ _ Hi Hj') [-]Q _ (Nat.lt_le_incl _ _ (H _ _ Hi Hj'))))) [-] Sumx (fun (i : nat) (Hi : i < n) => Sum2 (fun (j : nat) (Hj : sub i <= j) (Hj' : j <= pred (sub (S i))) => Part F (fQ j (H _ _ Hi Hj')) just2[*] (Q _ (H' _ _ Hi Hj') [-]Q _ (Nat.lt_le_incl _ _ (H _ _ Hi Hj')))))) [=] AbsIR (Sumx (fun (i : nat) (Hi : i < n) => Sum2 (fun (j : nat) (Hj : sub i <= j) (Hj' : j <= pred (sub (S i))) => Part F (fP i Hi) just1[*] (Q _ (H' _ _ Hi Hj') [-]Q _ (Nat.lt_le_incl _ _ (H _ _ Hi Hj'))) [-] Part F (fQ j (H _ _ Hi Hj')) just2[*] (Q _ (H' _ _ Hi Hj') [-]Q _ (Nat.lt_le_incl _ _ (H _ _ Hi Hj')))))).
proof: Proof. apply AbsIR_wd. eapply eq_transitive_unfolded. apply Sumx_minus_Sumx. apply Sumx_wd; intros. eapply eq_transitive_unfolded. apply Sum2_minus_Sum2. apply RL_sub_SS. algebra. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef