proposition: Lemma Alembert_C2_aux_positivity : forall Xn : nat -> R, let Yn i := (2 * Rabs (Xn i) + Xn i) / 2 in (forall n, Xn n <> 0) -> forall n, 0 < Yn n.
proof: Proof. intros Xn Yn H n; unfold Yn; unfold Rdiv; rewrite <- (Rmult_0_r (/ 2)); rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l. - apply Rinv_0_lt_compat; prove_sup0. - apply Rplus_lt_reg_l with (- Xn n); rewrite Rplus_0_r; unfold Rminus; rewrite (Rplus_comm (- Xn n)); rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; apply Rle_lt_trans with (Rabs (Xn n)). + rewrite <- Rabs_Ropp; apply RRle_abs. + rewrite <-Rplus_diag; pattern (Rabs (Xn n)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra