proposition: Lemma sep__part_Sum : AbsIR (Partition_Sum gP incF[-]Partition_Sum sep__part_pts_in_Partition incF)[<=] alpha.
proof: Proof. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply sep__part_Sum3. eapply leEq_transitive. 2: apply sep__part_Sum4. eapply leEq_transitive. apply triangle_SumxIR. apply Sumx_resp_leEq; intros. eapply leEq_transitive. apply triangle_Sum2IR. rewrite (Nat.lt_succ_pred (sep__part_fun i (Nat.lt_le_incl _ _ H)) (sep__part_fun (S i) H) (sep__part_fun_mon _ _ _ _ (Nat.lt_succ_diag_r i))). apply Nat.lt_le_incl; apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. apply Sum2_resp_leEq. rewrite (Nat.lt_succ_pred (sep__part_fun i (Nat.lt_le_incl _ _ H)) (sep__part_fun (S i) H) (sep__part_fun_mon _ _ _ _ (Nat.lt_succ_diag_r i))). apply Nat.lt_le_incl; apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. intros k Hk Hk'. elim (le_lt_dec m (S i)); intro. cut (S i = m); [ intro | clear Hk Hk'; lia ]. generalize H0. unfold m at 1 in |- *; elim RS'_delta2_delta4; intro; simpl in |- *; intro. cut (i < m); [ intro | assumption ]. apply leEq_wdl with (AbsIR ((F (g k (RS'_Hsep_S _ _ H Hk')) just1[-]F (g _ (sep__part_aux RS'_m1)) just1)[*] (P (S k) (RS'_Hsep_S _ _ H Hk')[-]P k (RS'_Hsep _ _ H Hk')))). 2: apply AbsIR_wd; apply mult_wdl. 2: apply cg_minus_wd; [ algebra | idtac ]. 2: cut (i = RS'_m1); [ intro | auto ]. 2: generalize H; rewrite H3; intro. 2: unfold sep__part_pts in |- *; simpl in |- *; algebra. elim (le_lt_dec (pred (sep__part_h (S RS'_m1))) k); intro. cut (pred (sep__part_h (S RS'_m1)) = k); intros. apply leEq_wdl with ZeroR. astepl (([0][+][0])[*]ZeroR). apply mult_resp_leEq_both. apply eq_imp_leEq; algebra. apply leEq_reflexive. apply plus_resp_leEq_both; unfold M in |- *; apply positive_norm. apply less_leEq; astepr (delta [/]TwoNZ); apply pos_div_two; exact RS'_delta_pos. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply AbsIRz_isz. apply AbsIR_wd. rstepr ((F (g _ (sep__part_aux RS'_m1)) just1[-]F (g _ (sep__part_aux RS'_m1)) just1)[*] (P (S k) (RS'_Hsep_S _ _ H Hk')[-]P k (RS'_Hsep _ _ H Hk'))). algebra. cut (forall H, sep__part_fun (S i) H = n). intro. cut (sep__part_h (S RS'_m1) = n); intros. rewrite H4 in a2. rewrite H3 in Hk'. rewrite H4. apply Nat.le_antisymm; auto. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros. auto. rewrite H0; exact sep__part_fun_m. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. eapply leEq_transitive. apply triangle_IR_minus. apply plus_resp_leEq_both; unfold M, I in |- *; apply norm_bnd_AbsIR; apply Pts_part_lemma with n P; apply gP. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (P k (RS'_Hsep i k H Hk')); apply prf2. apply sep__part_h_lemma3 with i. rewrite sep__part_fun_i in Hk; assumption. rewrite H1; assumption. apply leEq_wdl with (AbsIR ((F (g k (RS'_Hsep_S _ _ H Hk')) just1[-]F (g _ (sep__part_aux i)) just1)[*] (P (S k) (RS'_Hsep_S _ _ H Hk')[-]P k (RS'_Hsep _ _ H Hk')))). 2: apply AbsIR_wd; apply mult_wd. 2: apply cg_minus_wd; apply pfwdef; [ algebra | unfold sep__part_pts in |- *; apply gP' ]; auto. 2: apply cg_minus_wd; apply prf1; auto. elim (le_lt_dec (pred (sep__part_h RS'_m1)) k); intro. elim (le_lt_eq_dec _ _ a1); intro. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. eapply leEq_transitive. apply triangle_IR_minus. apply plus_resp_leEq_both; unfold M, I in |- *; apply norm_bnd_AbsIR; apply Pts_part_lemma with n P; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (P k (RS'_Hsep i k H Hk')); apply prf2. apply less_leEq; eapply leEq_less_trans. 2: apply b0. unfold cg_minus in |- *; apply plus_resp_leEq_both. apply Partition_mon. rewrite <- (Nat.lt_succ_pred (sep__part_h RS'_m1) (sep__part_h (S RS'_m1))). apply le_n_S. cut (forall H, sep__part_h (S RS'_m1) = sep__part_fun (S i) H); intros. rewrite (H2 H); assumption. generalize H2; rewrite H0. intro; rewrite sep__part_fun_m. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; auto. apply sep__part_h_mon_3. elim (ProjT2 sep__part_app_n); fold RS'_m1 in |- *; intros. apply H3; apply le_n. apply Nat.lt_succ_diag_r. apply inv_resp_leEq; apply Partition_mon. eapply Nat.le_trans. 2: apply a2. clear Hk Hk'; lia. apply leEq_wdl with ZeroR. astepl (([0][+][0])[*]ZeroR). apply mult_resp_leEq_both. apply eq_imp_leEq; algebra. apply leEq_reflexive. apply plus_resp_leEq_both; unfold M in |- *; apply positive_norm. apply less_leEq; astepr (delta [/]TwoNZ); apply pos_div_two; exact RS'_delta_pos. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply AbsIRz_isz. apply AbsIR_wd. rstepr ((F (g _ (sep__part_aux i)) just1[-]F (g _ (sep__part_aux i)) just1)[*] (P (S k) (RS'_Hsep_S _ _ H Hk')[-]P k (RS'_Hsep _ _ H Hk'))). apply mult_wdl. apply cg_minus_wd; apply pfwdef; apply gP'; auto. rewrite H1; auto. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. eapply leEq_transitive. apply triangle_IR_minus. apply plus_resp_leEq_both; unfold M, I in |- *; apply norm_bnd_AbsIR; apply Pts_part_lemma with n P; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (P k (RS'_Hsep i k H Hk')); apply prf2. apply sep__part_h_lemma3 with i. rewrite sep__part_fun_i in Hk; assumption. rewrite H1; assumption. elim (le_lt_eq_dec _ _ Hk'); intro. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. eapply leEq_transitive. apply triangle_IR_minus. apply plus_resp_leEq_both; unfold M, I in |- *; apply norm_bnd_AbsIR. apply Pts_part_lemma with n P; assumption. apply Pts_part_lemma with sep__part_length sep__part; apply sep__part_pts_in_Partition. cut (pred (sep__part_fun (S i) H) <= n); intros. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl (P k (RS'_Hsep i k H Hk')); apply prf2. apply sep__part_h_lemma3 with i. rewrite sep__part_fun_i in Hk; assumption. rewrite sep__part_fun_i in a0; assumption. apply Nat.le_trans with (sep__part_fun (S i) H). auto with arith. apply sep__part_fun_bnd. apply leEq_wdl with ZeroR. astepl (([0][+][0])[*]ZeroR). apply mult_resp_leEq_both. apply eq_imp_leEq; algebra. apply leEq_reflexive. apply plus_resp_leEq_both; unfold M in |- *; apply positive_norm. apply less_leEq; astepr (delta [/]TwoNZ); apply pos_div_two; exact RS'_delta_pos. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply AbsIRz_isz. apply AbsIR_wd. rstepr ((F (g _ (sep__part_aux i)) just1[-]F (g _ (sep__part_aux i)) just1)[*] (P (S k) (RS'_Hsep_S _ _ H Hk')[-]P k (RS'_Hsep _ _ H Hk'))). apply mult_wdl. apply cg_minus_wd; apply pfwdef; unfold sep__part_pts in |- *; apply gP'; auto. rewrite sep__part_fun_i in b1; assumption. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)