proposition: Lemma ref_calc8 : 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')))))) [<=] Sumx (fun (i : nat) (Hi : i < n) => Sum2 (fun (j : nat) (Hj : sub i <= j) (Hj' : j <= pred (sub (S i))) => e[*] (Q _ (H' _ _ Hi Hj') [-]Q _ (Nat.lt_le_incl _ _ (H _ _ Hi Hj'))))).
proof: Proof. apply Sumx_resp_leEq; intros. apply Sum2_resp_leEq. apply RL_sub_SS. intros j Hj Hj'. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both. apply AbsIR_nonneg. apply AbsIR_nonneg. generalize (proj2b_sig2T _ _ _ (contF' e He)); fold d in |- *; intros. apply H2. unfold I in |- *; apply Pts_part_lemma with n P; assumption. unfold I in |- *; apply Pts_part_lemma with m Q; assumption. apply leEq_transitive with (Mesh P). 2: assumption. apply leEq_transitive with (AbsIR (P (S i) H1[-]P i (Nat.lt_le_incl _ _ H1))). 2: eapply leEq_wdl. 3: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply Mesh_lemma. 2: apply shift_leEq_minus; astepl (P i (Nat.lt_le_incl _ _ H1)); apply prf2. apply compact_elements with (prf2 _ _ _ _ P i (Nat.lt_le_incl _ _ H1) H1). apply HfP. elim (HfQ j (H _ _ H1 Hj')); intros. split. elim (RL_sub_hyp i (Nat.lt_le_incl _ _ H1)); intros. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply p. apply leEq_transitive with (Q j (Nat.lt_le_incl _ _ (H i j H1 Hj'))). apply Partition_mon; assumption. assumption. elim (RL_sub_hyp (S i) H1); intros. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply p. apply leEq_transitive with (Q _ (H i j H1 Hj')). assumption. apply Partition_mon. rewrite <- (Nat.lt_succ_pred _ _ (RL_sub_S i)); auto with arith. apply eq_imp_leEq; apply AbsIR_eq_x. apply shift_leEq_minus; astepl (Q j (Nat.lt_le_incl _ _ (H _ _ H1 Hj'))); apply prf2. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef