proposition: Lemma prod_minus : forall f n, prod f n - prod f (S n) == ([1-]f n) * prod f n.
proof: Proof. intros f n; rewrite prod_S. apply Oeq_trans with (1 * prod f n - f n * prod f n). rewrite Umult_one_left; auto. rewrite <- Uminus_distr_left; auto. Qed.
imports: ALEA(Utheory)