proposition: Lemma ref_calc7 : Sumx (fun (i : nat) (Hi : i < n) => AbsIR (Sum2 (fun (j : nat) (Hj : sub i <= j) (Hj' : j <= pred (sub (S i))) => (Part F (fP i Hi) just1[-]Part F (fQ j (H _ _ Hi Hj')) just2) [*] (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))) => AbsIR ((Part F (fP i Hi) just1[-]Part F (fQ j (H _ _ Hi Hj')) just2) [*] (Q _ (H' _ _ Hi Hj') [-]Q _ (Nat.lt_le_incl _ _ (H _ _ Hi Hj')))))).
proof: Proof. apply Sumx_resp_leEq; intros. eapply leEq_wdr. apply triangle_Sum2IR. apply RL_sub_SS. algebra. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef