proposition: Lemma continued_fraction_correct v n : eval_continued_fraction (continued_fraction v n) == v.
proof: Proof. cbv [eval_continued_fraction]. revert v; induction n; intro; cbn; destruct (Qeq_bool 0 v) eqn:H; cbn. all: rewrite ?Qeq_bool_iff in H; rewrite <- ?H. all: try reflexivity. { rewrite (surjective_pairing (continued_fraction _ _)); cbn. rewrite IHn. cbv [Qdiv]; rewrite !Qmult_1_l, Qinv_involutive. ring. } Qed.
imports: Coq.Strings.String Coq.Structures.Orders Coq.micromega.Lia Coq.Bool.Bool Coq.Sorting.Mergesort Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax Coq.NArith.NArith Coq.ZArith.ZArith Coq.Arith.Arith Coq.Lists.List PerformanceExperiments.LetIn