proposition: Lemma prod_eq_compat : forall (f g: nat -> U) (n:nat), (forall k, (k < n)%nat -> f k == g k) -> (prod f n) == (prod g n).
proof: Proof. induction n; auto. intros; repeat rewrite prod_S. apply Oeq_trans with (g n * prod f n); auto with arith. Qed.
imports: ALEA(Utheory)