proposition: Lemma Lim_const : forall x : IR, x [=] Lim (Cauchy_const x).
proof: Proof. intros. apply Limits_unique. red in |- *; intro; exists 0. intros; unfold Cauchy_const in |- *; simpl in |- *. astepr ZeroR; apply zero_AbsSmall; apply less_leEq; assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)