proposition: Lemma ref_calc1 : forall (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'))) [=] P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi).
proof: Proof. intros. unfold Sum2 in |- *. elim (RL_sub_hyp (S i) Hi); intros P1 HP1. elim (RL_sub_hyp i (Nat.lt_le_incl _ _ Hi)); intros P2 HP2. apply eq_transitive_unfolded with (Q _ P1[-]Q _ P2). 2: apply eq_symmetric_unfolded; apply cg_minus_wd; [ apply HP1 | apply HP2 ]. cut (sub (S i) = S (pred (sub (S i)))). 2: symmetry; apply Nat.lt_succ_pred with 0; apply RL_sub_S. intro. generalize P1 HP1; clear HP1 P1. pattern (sub (S i)) at 1 2 11 in |- *. rewrite H1; intros. eapply eq_transitive_unfolded. apply str_Mengolli_Sum_gen with (f := h). apply RL_sub_SS. intros j Hj Hj'. elim (le_lt_dec j (pred (sub (S i)))); intro; simpl in |- *. elim (le_lt_dec (sub i) j); intro; simpl in |- *. unfold h in |- *. apply cg_minus_wd. elim (le_lt_dec (S j) m); intro; simpl in |- *. apply prf1; auto. cut (S j <= m); [ intro | apply H' with i; assumption ]. exfalso; apply (proj1 (Nat.le_ngt _ _) H2 b0). elim (le_lt_dec j m); intro; simpl in |- *. apply prf1; auto. cut (j < m); [ intro | apply H with i; assumption ]. exfalso; apply Nat.le_ngt with m j; auto with arith. exfalso; apply Nat.le_ngt with (sub i) j; auto with arith. exfalso; apply (proj1 (Nat.le_ngt _ _) Hj' b0). unfold h in |- *. apply cg_minus_wd. elim (le_lt_dec (S (pred (sub (S i)))) m); intro; simpl in |- *. apply prf1; auto. exfalso. apply (proj1 (Nat.le_ngt _ _) P1 b0). elim (le_lt_dec (sub i) m); intro; simpl in |- *. apply prf1; auto. exfalso. apply (proj1 (Nat.le_ngt _ _) P2 b0). Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef