fact: Fixpoint numden_Rcontfrac_tailrecB (accu: list bigZ) (n1 d1: bigZ) (n2 d2: bigZ) (fuel: nat) {struct fuel}: (list bigZ * bigQ * bigQ) := let default := (rev_append accu nil, BigQ.div (BigQ.Qz n1) (BigQ.Qz d1), BigQ.div (BigQ.Qz n2) (BigQ.Qz d2)) in match fuel with | O => default | S fuel' => let '(q1, r1) := BigZ.div_eucl n1 d1 in let '(q2, r2) := BigZ.div_eucl n2 d2 in match BigZ.eqb q1 q2 with | false => default | true => let r1_is_zero := BigZ.eqb r1 0 in let r2_is_zero := BigZ.eqb r2 0 in match Bool.eqb r1_is_zero r2_is_zero with | false => default | true => match r1_is_zero with | true => match BigZ.eqb q1 1 with | true => (rev_append accu nil, 1%bigQ, 1%bigQ) | false => (rev_append ((q1 - 1)%bigZ :: accu) nil, 1%bigQ, 1%bigQ) end | false => numden_Rcontfrac_tailrecB (q1 :: accu) d1 r1 d2 r2 fuel' end end end end.
imports: Bignums.BigQ.BigQ