proposition: Lemma prod_SO_pos : forall (An:nat -> R) (N:nat), (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_R0 An N.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; apply H; trivial. - simpl; apply Rmult_le_pos. + apply HrecN; intros; apply H; apply Nat.le_trans with N; [ assumption | apply Nat.le_succ_diag_r ]. + apply H; apply Nat.le_refl. Qed.
imports: Compare Rbase Rfunctions Rseries PartSum Binomial Lia