proposition: Lemma limit_le_unique : forall f l1 l2, is_limit f l1 -> is_limit f l2 -> l1 <= l2.
proof: Proof. intros f l1 l2 liml1 liml2; apply Ule_lt_half_exp; intro p2. intros; apply Ule_lt_half_exp; intro p1. apply (liml1 p1); auto; intros M1 H1. apply (liml2 p2); auto; intros M2 H2. case (H1 (M1+M2)%nat); auto with arith; intros. case (H2 (M1+M2))%nat; auto with arith; intros. apply Ole_trans with (f (M1 + M2)%nat + [1/2]^p1); auto. Qed.
imports: ALEA(Utheory)