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