proposition: Lemma prod_decr : forall (f : nat -> U) (n m:nat), (n <= m)%nat -> prod f m <= prod f n.
proof: Proof. intros f n m H; induction H; auto. intros; rewrite prod_S. apply Ole_trans with (2:=IHle); auto. Qed.
imports: ALEA(Utheory)