proposition: Lemma Nfinite_prod_eq_compat : forall n f g, (forall k, f k = g k) -> Nfinite_prod_0_n n f = Nfinite_prod_0_n n g.
proof: Proof. intros. apply Nfinite_prod_subtle_eq_compat. intros. apply H. Qed.
imports: Arith Compare Nk_ind Npow Ndiv