proposition: Lemma fact_prodSO : forall n:nat, INR (fact n) = prod_f_R0 (fun k:nat => (match (eq_nat_dec k 0) with | left _ => 1%R | right _ => INR k end)) n.
proof: Proof. intro; induction n as [| n Hrecn]. - reflexivity. - simpl; rewrite <- Hrecn. case n; auto with real. intros; repeat rewrite plus_INR;rewrite mult_INR;ring. Qed.
imports: Compare Rbase Rfunctions Rseries PartSum Binomial Lia