proposition: Lemma is_finite_correct (x : Rbar) : is_finite x <-> exists y : R, x = Finite y.
proof: Proof. rewrite /is_finite ; case: x => /= ; split => // H. by exists r. by case: H. by case: H. Qed.
imports: Coq(Reals ssreflect) Rcomplements