proposition: Lemma retract_lt : forall (f : nat -> U) (n : nat), sigma f n < 1 -> retract f n.
proof: Proof. induction n; auto. rewrite sigma_S. intros;assert ((sigma f n)<1). apply Ule_lt_trans with (f n + sigma f n); auto. assert (f n <= [1-](sigma f n)); auto. apply Uplus_lt_Uinv; auto. Qed.
imports: ALEA(Utheory)