fact: Fixpoint Zpos_div_eucl_aux1 (a b : positive) {struct b} := match b with | xO b' => match a with | xO a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r)%Z | xI a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r + 1)%Z | xH => (Z0, Zpos a) end | xH => (Zpos a, Z0) | xI _ => Z.pos_div_eucl a (Zpos b) end.
imports: Coq(ZArith Lia Zquot)