proposition: Lemma rep_L_inv: forall alpha r, rep (Cons LL alpha) r -> rep alpha ((3*r+1)/(-r+1))%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 |]; rewrite <- R_addenda.Rdiv_Ropp_numerator; auto; rewrite R_addenda.Rdiv_Rmult_numerator; auto; repeat rewrite R_addenda.Rdiv_Rplus_Rmult; auto; rewrite R_addenda.Rdiv_Rdiv_simplify; auto. transitivity (x/1)%R; [field; auto|]; apply Rmult_Rdiv; auto; [| ring]; stepl 4%R; auto; ring. stepl 4%R; auto; ring. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs