proposition: Lemma first_refinement_lemma : AbsIR (Partition_Sum HfP incF[-]Partition_Sum HfQ incF) [<=] e[*] (b[-]a).
proof: Proof. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply ref_calc2. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply ref_calc3. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply ref_calc4. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply ref_calc5. eapply leEq_transitive. apply ref_calc6. eapply leEq_transitive. apply ref_calc7. eapply leEq_transitive. apply ref_calc8. apply leEq_wdl with (e[*] Sumx (fun (i : nat) (Hi : i < n) => 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'))))). apply mult_resp_leEq_lft. 2: apply less_leEq; assumption. apply leEq_wdl with (Sumx (fun (i : nat) (Hi : i < n) => P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))). 2: apply Sumx_wd; intros. 2: apply eq_symmetric_unfolded; apply ref_calc1. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply Mengolli_Sum with (f := fun (i : nat) (Hi : i <= n) => P i Hi). eapply leEq_transitive. apply leEq_AbsIR. eapply leEq_wdr. 2: apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl a; assumption. apply compact_elements with Hab; apply Partition_in_compact. red in |- *; intros; apply prf1; auto. intros; apply cg_minus_wd; apply prf1; auto. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply Sumx_comm_scal'. apply Sumx_wd; intros. eapply eq_transitive_unfolded. 2: apply Sum2_comm_scal'. algebra. apply RL_sub_SS. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef