proposition: Lemma abs_pow_ltRe : forall s, (forall i, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c) -> forall i, AbsIR (Re (s (S i)) [-]Re (s i)) [<=] nrtq[^]i[*]nrtc.
proof: Proof. intros s H i. apply leEq_wdl with (AbsIR (Re (s (S i) [-]s i))). apply leEq_transitive with (AbsCC (s (S i) [-]s i)). apply absCC_absIR_re. generalize (H i). intro Hi. cut ([0] [<=] q[^]i[*]c). intro H0. cut (AbsCC (s (S i) [-]s i) [<=] NRoot H0 lt0n). intro H1. apply leEq_wdr with (NRoot H0 lt0n). assumption. apply nrt_pow. apply power_cancel_leEq with n. auto with arith. apply NRoot_nonneg. apply leEq_wdr with (q[^]i[*]c). exact (H i). algebra. apply mult_resp_nonneg. apply nexp_resp_nonneg. assumption. apply less_leEq; assumption. apply ABSIR_wd. apply Re_resp_inv. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)