proposition: Lemma Nfinite_prod_0_absord : forall n f k, k <= n -> f k = 0 -> Nfinite_prod_0_n n f = 0.
proof: Proof. induction n. intros. compute. apply Nat.le_0_r in H. rewrite H in H0. exact H0. intros. rewrite Nfinite_prod_split_upper. apply le_le_S_eq in H. destruct H. rewrite IHn with f k. ring. auto with arith. exact H0. rewrite <- H. rewrite H0. ring. Qed.
imports: Arith Compare Nk_ind Npow Ndiv