proposition: Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n).
proof: Proof. intro; apply lt_INR_0; apply Nat.neq_0_lt_0; red; intro; elim (fact_neq_0 n); assumption. Qed.
imports: Compare Rbase Rfunctions Rseries PartSum Binomial Lia