proposition: Lemma Nfinite_prod_split_lower : forall n f, Nfinite_prod_0_n (S n) f = (f 0) * (Nfinite_prod_0_n n (fun k => f (S k))).
proof: Proof. induction n. intros. unfold Nfinite_prod_0_n. reflexivity. intros. rewrite Nfinite_prod_split_upper. rewrite IHn. rewrite Nfinite_prod_split_upper. ring. Qed.
imports: Arith Compare Nk_ind Npow Ndiv