proposition: Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0.
proof: Proof. intro; red; intro; apply (not_O_INR (fact n) (fact_neq_0 n)); assumption. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac