proposition: Lemma retract_unif : forall (f : nat -> U) (n : nat), (forall k, (k<=n)%nat -> f k <= [1/]1+n) -> retract f (S n).
proof: Proof. red; intros. apply Ole_trans with ([1/]1+n); auto with arith. apply Uinv_le_perm_right. apply Ole_trans with (sigma (fun k => [1/]1+n) n); auto. apply Ole_trans with (sigma f n); auto with arith. apply Uinv_le_perm_right; auto. Qed.
imports: ALEA(Utheory)