proposition: Lemma simpl_fact : forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n).
proof: Proof. intro; rewrite (Rinv_inv (INR (fact n))); unfold fact at 1; cbv beta iota; fold fact; rewrite (mult_INR (S n) (fact n)); rewrite (Rinv_mult (INR (S n)) (INR (fact n))). rewrite (Rmult_assoc (/ INR (S n)) (/ INR (fact n)) (INR (fact n))); rewrite (Rinv_l (INR (fact n)) (INR_fact_neq_0 n)); apply (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1). Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac