proposition: Lemma rep_stepl: forall alpha beta x, rep alpha x -> bisim alpha beta -> rep beta x.
proof: Proof. cofix. intros [[ | | ] alpha] [[ | | ] beta] x h_rep h_bisim; try (inversion h_bisim; discriminate H). inversion_clear h_rep as [alpha0 dummy x0 H_x0 h_rep0 h_bisim0|alpha0 dummy x0 H_x0 h_rep0 h_bisim0|alpha0 dummy x0 H_x0 h_rep0 h_bisim0]; try (inversion h_bisim0; discriminate H) || apply (rep_L alpha (Cons LL beta) x0 H_x0); [ apply (rep_stepl alpha0); trivial;inversion h_bisim0 | ] ; unfold bisim; apply sym_EqSt ; trivial. inversion_clear h_rep as [alpha0 dummy x0 H_x0 h_rep0 h_bisim0|alpha0 dummy x0 H_x0 h_rep0 h_bisim0|alpha0 dummy x0 H_x0 h_rep0 h_bisim0]; try (inversion h_bisim0; discriminate H) || apply (rep_R alpha (Cons RR beta) x0 H_x0); [ apply (rep_stepl alpha0); trivial;inversion h_bisim0 | ] ; unfold bisim; apply sym_EqSt ; trivial. inversion_clear h_rep as [alpha0 dummy x0 H_x0 h_rep0 h_bisim0|alpha0 dummy x0 H_x0 h_rep0 h_bisim0|alpha0 dummy x0 H_x0 h_rep0 h_bisim0]; try (inversion h_bisim0; discriminate H) || apply (rep_M alpha (Cons MM beta) x0 H_x0); [ apply (rep_stepl alpha0); trivial;inversion h_bisim0 | ] ; unfold bisim; apply sym_EqSt ; trivial. Qed.
imports: digits Refining_M Streams_addenda Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs