fact: Fixpoint pos_div_eucl (a:positive) (b:Z) : Z * Z := match a with | xH => if 2 <=? b then (0, 1) else (1, 0) | xO a' => let (q, r) := pos_div_eucl a' b in let r' := 2 * r in if r' <? b then (2 * q, r') else (2 * q + 1, r' - b) | xI a' => let (q, r) := pos_div_eucl a' b in let r' := 2 * r + 1 in if r' <? b then (2 * q, r') else (2 * q + 1, r' - b) end.
imports: BinNums BinPos BinNat