proposition: Lemma ref_calc3 : AbsIR (Sumx (fun (i : nat) (Hi : i < n) => Part F (fP i Hi) just1[*] Sum2 (fun (j : nat) (Hj : sub i <= j) (Hj' : j <= pred (sub (S i))) => 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'))))) [-] 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')))))).
proof: Proof. apply AbsIR_wd. apply cg_minus_wd; apply Sumx_wd; intros. apply eq_symmetric_unfolded; apply Sum2_comm_scal' with (f := fun (j : nat) (Hj : sub i <= j) (Hj' : j <= pred (sub (S i))) => Q (S j) (H' _ _ H1 Hj') [-]Q j (Nat.lt_le_incl _ _ (H _ _ H1 Hj'))). apply RL_sub_SS. algebra. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef