proposition: Lemma prod_S_lift : forall (f :nat -> U) (n:nat), prod f (S n) == (f O) * (prod (fun k => f (S k)) n).
proof: Proof. intros f n; generalize f; induction n; simpl; intros; auto. rewrite prod_S. rewrite IHn. rewrite prod_S. rewrite Umult_assoc. rewrite (Umult_sym (f0 (S n)) (f0 O)); auto. Qed.
imports: ALEA(Utheory)