proposition: Lemma prod_SO_Rle : forall (An Bn:nat -> R) (N:nat), (forall n:nat, (n <= N)%nat -> 0 <= An n <= Bn n) -> prod_f_R0 An N <= prod_f_R0 Bn N.
proof: Proof. intros; induction N as [| N HrecN]. - elim H with O; trivial. - simpl; apply Rle_trans with (prod_f_R0 An N * Bn (S N)). + apply Rmult_le_compat_l. * apply prod_SO_pos; intros; elim (H n (Nat.le_trans _ _ _ H0 (Nat.le_succ_diag_r N))); intros; assumption. * elim (H (S N) (le_n (S N))); intros; assumption. + do 2 rewrite <- (Rmult_comm (Bn (S N))); apply Rmult_le_compat_l. * elim (H (S N) (le_n (S N))); intros. apply Rle_trans with (An (S N)); assumption. * apply HrecN; intros; elim (H n (Nat.le_trans _ _ _ H0 (Nat.le_succ_diag_r N))); intros; split; assumption. Qed.
imports: Compare Rbase Rfunctions Rseries PartSum Binomial Lia