fact: Fixpoint continued_fraction (v : Q) (count : nat) : list Z * Q := if Qeq_bool 0 v then ([], 0) else match count with | O => ([], v) | S count => let a0 := Qfloor v in let rem := 1 / (v - a0) in let '(rest, rem) := continued_fraction rem count in (a0 :: rest, rem) end.
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