proposition: Lemma Nfactorial_is_finite_prod : forall n, fact (S n) = Nfinite_prod_0_n n (fun k => S k).
proof: Proof. induction n. compute. reflexivity. assert (fact (S(S n))=S(S n)*fact(S n)). compute. reflexivity. rewrite H. clear H. rewrite Nfinite_prod_split_upper. rewrite IHn. ring. Qed.
imports: Arith Compare Nk_ind Npow Ndiv