Coq proof that 0.9999999999 = 1

dotnineninenine_is_one

(* Proof that 0.9999999999... = 1 *)

Require Import Reals.
From Coquelicot Require Import Coquelicot.
Require Import Psatz.

Definition nine i := (9/10)*(1/10)^i.

Example e1: sum_n nine 3 = 9/10 + 9/100 + 9/1000 + 9/10000.
  unfold nine.
  repeat rewrite sum_Sn, ?sum_O.
  unfold plus; simpl; lra.
Qed.

Lemma nines: Series nine = 1.
  unfold nine.
  rewrite Series_scal_l.
  enough ( Series (pow (1 / 10)) = 10 / 9) by lra.
  apply is_series_unique.
  evar (e:R).
  replace (10/9) with e.
  apply is_series_geom.
  unfold Rabs; case Rcase_abs; lra.
  unfold e; lra.
Qed.