proposition: Lemma prod_zero : forall f n k, (k<n)%nat -> f k ==0 -> prod f n==0.
proof: Proof. induction n; simpl; intros; auto. absurd ((k < 0)%nat); auto with arith. rewrite prod_S. assert (k < n \/ k = n)%nat. lia. case H1; intros; subst; auto. rewrite (IHn k); auto. rewrite H0; auto. Qed.
imports: ALEA(Utheory)