proposition: Lemma Nfinite_prod_split_upper : forall n f, Nfinite_prod_0_n (S n) f = (Nfinite_prod_0_n n f) * (f (S n)).
proof: Proof. unfold Nfinite_prod_0_n. fold Nfinite_prod_0_n. reflexivity. Qed.
imports: Arith Compare Nk_ind Npow Ndiv