proposition: Lemma Nfinite_prod_mult_compat : forall n f a g, (forall k, k <= n -> f k = a * g k) -> Nfinite_prod_0_n n f = a^(S n) * Nfinite_prod_0_n n g.
proof: Proof. induction n. intros. unfold Nfinite_prod_0_n. unfold Nat.pow. rewrite Nat.mul_1_r. apply H. auto with arith. intros. rewrite Nfinite_prod_split_upper. rewrite Nfinite_prod_split_upper. rewrite H. rewrite IHn with f a g. rewrite Npower_succ. rewrite Npower_succ. rewrite Npower_succ. ring. intros. apply H. auto with arith. auto with arith. Qed.
imports: Arith Compare Nk_ind Npow Ndiv