proposition: Lemma rep_M_inv: forall alpha r, rep (Cons MM alpha) r -> rep alpha (3*r)%R.
proof: Proof. intros alpha r H_rep; inversion H_rep as [alpha0 beta x [H1 H2] H_rep0 H_bisim H3 H_rx |alpha0 beta x [H1 H2] H_rep0 H_bisim H3 H_rx |alpha0 beta x [H1 H2] H_rep0 H_bisim H3 H_rx]; try (inversion H_bisim as [H4 H5]; discriminate H4); destruct H_bisim; stepr x; [ stepl alpha0; trivial; unfold bisim; apply sym_EqSt ; trivial |]; field; auto. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs