proposition: Lemma has_limit_inv : forall f : nat -> U, has_lim f -> has_lim (fun x => [1-]f x).
proof: Proof. unfold has_lim; intros. apply Ole_trans with ([1-]liminf f); auto. apply Ole_trans with ([1-]limsup f); auto. Qed.
imports: ALEA(Utheory)