proposition: Lemma SublemmaIm : forall s, (forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) -> forall N m, N <= m -> AbsIR (Im (s m) [-]Im (s N)) [<=] (nrtq[^]m[-]nrtq[^]N[/] nrtq[-][1][//]nrtq_) [*]nrtc.
proof: Proof. intros s Hi N m leNm. elim (le_lt_eq_dec N m leNm). intro ltNm. generalize (diff_is_sum (fun j : nat => Im (s j)) N m ltNm). intro HSum. generalize (ABSIR_wd _ _ HSum). intro Habseq. apply leEq_wdl with (ABSIR (Sum N (pred m) (fun i : nat => Im (s (S i)) [-]Im (s i)))). 2: apply eq_symmetric_unfolded; apply Habseq. cut (N <= S (pred m)). intro leNm'. 2: clear nrtq_ nrtqlt1 nrtc nrtq; lia. generalize (triangle_SumIR N (pred m) (fun i : nat => Im (s (S i)) [-]Im (s i)) leNm'). intro Htri. apply leEq_transitive with (Sum N (pred m) (fun i : nat => csf_fun IR IR AbsIR (Im (s (S i)) [-]Im (s i)))). exact Htri. generalize (Sum_pres_leEq (fun i : nat => AbsIR (Im (s (S i)) [-]Im (s i))) (fun i : nat => nrtq[^]i[*]nrtc) (abs_pow_ltIm s Hi) N ( pred m)). intro Hlt. apply leEq_transitive with (Sum N (pred m) (fun i : nat => nrtq[^]i[*]nrtc)). cut (N <= pred m). intro leNpm. exact (Hlt leNpm). generalize (Nat.lt_succ_pred N m ltNm). intro Heq. symmetry in Heq. apply Nat.lt_succ_r. simpl in |- *. rewrite <- Heq. assumption. generalize (Sum_c_exp nrtq nrtq_ N (pred m)). intro Hs. generalize (Sum_comm_scal (fun i : nat => nrtq[^]i) nrtc N (pred m)). intro Hs2. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply Hs2. apply mult_resp_leEq_rht. generalize (Sum_c_exp nrtq nrtq_ N (pred m)). intro Hs3. cut (S (pred m) = m). intro Heq. rewrite Heq in Hs3. apply eq_imp_leEq; assumption. generalize (Nat.lt_succ_pred N m ltNm). auto. exact (less_leEq _ _ _ zlt_nrtc). intro HNm. rewrite HNm. apply leEq_wdl with (AbsIR [0]). apply leEq_wdl with ZeroR. apply leEq_wdr with ZeroR. exact (leEq_reflexive _ _). rational. apply eq_symmetric_unfolded; exact AbsIRz_isz. apply ABSIR_wd. rational. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)