proposition: Lemma sep__part_suRS'_m1 : forall (i : nat) (Hi : i < m), Sum2 (fun (j : nat) (Hj : sep__part_fun i (Nat.lt_le_incl _ _ Hi) <= j) (Hj' : j <= pred (sep__part_fun (S i) Hi)) => P _ (RS'_Hsep_S _ _ _ Hj')[-]P _ (RS'_Hsep _ _ _ Hj'))[=] sep__part _ Hi[-]sep__part _ (Nat.lt_le_incl _ _ Hi).
proof: Proof. intros; simpl in |- *. unfold Sum2 in |- *. cut (sep__part_fun (S i) Hi = S (pred (sep__part_fun (S i) Hi))). 2: symmetry; apply Nat.lt_succ_pred with (sep__part_fun i (Nat.lt_le_incl _ _ Hi)); apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. intro. cut (S (pred (sep__part_fun (S i) Hi)) <= n). 2: rewrite <- H; apply sep__part_fun_bnd. intro. apply eq_transitive_unfolded with (P _ H0[-]P _ (sep__part_fun_bnd i (Nat.lt_le_incl _ _ Hi))). 2: apply cg_minus_wd; apply prf1; auto. eapply eq_transitive_unfolded. apply str_Mengolli_Sum_gen with (f := h). rewrite <- H; apply Nat.lt_le_incl; apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. intro j; intros. do 2 elim le_lt_dec; intros; simpl in |- *. unfold h in |- *. do 2 elim le_lt_dec; intros; simpl in |- *. apply cg_minus_wd; apply prf1; auto. exfalso; apply Nat.le_ngt with j n. apply Nat.le_trans with (S j); auto with arith. assumption. exfalso; apply Nat.le_ngt with (S j) n. exact (RS'_Hsep_S _ _ Hi a1). assumption. exfalso; apply Nat.le_ngt with (S j) n. exact (RS'_Hsep_S _ _ Hi a1). assumption. exfalso; lia. exfalso; lia. exfalso; lia. unfold h in |- *. apply cg_minus_wd. elim le_lt_dec; simpl in |- *; intros. apply prf1; auto. exfalso; lia. elim le_lt_dec; intro; simpl in |- *. apply prf1; auto. exfalso; rewrite <- H in H0; apply Nat.le_ngt with (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) n. apply sep__part_fun_bnd. assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)