proposition: Lemma ref_calc2 : AbsIR (Partition_Sum HfP incF[-]Partition_Sum HfQ incF) [=] 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')))))).
proof: Proof. apply AbsIR_wd; unfold Partition_Sum in |- *. apply cg_minus_wd. apply Sumx_wd; intros. apply mult_wdr. apply eq_symmetric_unfolded; apply ref_calc1. apply eq_symmetric_unfolded; unfold Sum2 in |- *. apply eq_transitive_unfolded with (Sumx (fun (j : nat) (Hj : j < m) => part_tot_nat_fun _ _ (fun (i : nat) (H : i < m) => Part F (fQ i H) just2[*] (Q _ H[-]Q _ (Nat.lt_le_incl _ _ H))) j)). apply str_Sumx_Sum_Sum with (g := fun (i : nat) (Hi : i < n) (i0 : nat) => sumbool_rect (fun _ : {sub i <= i0} + {i0 < sub i} => IR) (fun _ : sub i <= i0 => sumbool_rect (fun _ : {i0 <= pred (sub (S i))} + {pred (sub (S i)) < i0} => IR) (fun a1 : i0 <= pred (sub (S i)) => Part F (fQ i0 (H i i0 Hi a1)) just2[*] (Q (S i0) (H' i i0 Hi a1) [-] Q i0 (Nat.lt_le_incl i0 m (H i i0 Hi a1)))) (fun _ : pred (sub (S i)) < i0 => [0]) (le_lt_dec i0 (pred (sub (S i))))) (fun _ : i0 < sub i => [0]) (le_lt_dec (sub i) i0)) (h := part_tot_nat_fun _ _ (fun (i : nat) (H : i < m) => Part F (fQ i H) just2[*] (Q _ H[-]Q _ (Nat.lt_le_incl _ _ H)))). exact RL_sub_0. exact RL_sub_mon. intros. elim (le_lt_dec (sub i) j); intro; simpl in |- *. elim (le_lt_dec j (pred (sub (S i)))); intro; simpl in |- *. unfold part_tot_nat_fun in |- *. elim (le_lt_dec m j); intro; simpl in |- *. exfalso. cut (0 < sub (S i)); [ intro | apply RL_sub_S ]. cut (sub (S i) <= m); intros. apply (proj1 (Nat.le_ngt _ _) H4); apply Nat.le_lt_trans with j; auto. rewrite <- RL_sub_n. apply RL_sub_mon'; apply Hi. apply mult_wd. apply pfwdef. apply HfQ'; auto. apply cg_minus_wd; apply prf1; auto. exfalso; apply (proj1 (Nat.le_ngt _ _) b0). rewrite (Nat.lt_succ_pred _ _ (RL_sub_S i)); auto. exfalso; apply (proj1 (Nat.le_ngt _ _) H1 b0). symmetry in |- *; apply RL_sub_n. apply Sumx_wd; intros. unfold part_tot_nat_fun in |- *. elim (le_lt_dec m i); intro; simpl in |- *. exfalso; apply Nat.le_ngt with m i; auto. apply mult_wd. apply pfwdef; apply HfQ'; auto. apply cg_minus_wd; apply prf1; auto. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef