proposition: Lemma prod_zero_elim : forall f n, prod f n==0 -> exc (fun k => (k<n)%nat /\ f k ==0).
proof: Proof. intros; apply class_exc; red; intros. assert (forall k, (k<n)%nat -> 0 < f k); intros. red; intro. apply H0. apply exc_intro with k; auto. absurd (0 < prod f n); auto. apply prod_not_zero; auto. Qed.
imports: ALEA(Utheory)