fact: Fixpoint div_eucl (a b : positive) {struct a} : N * N := match a with | xH => if 1 ?< b then (0%N, 1%N) else (1%N, 0%N) | xO a' => let (q, r) := div_eucl a' b in match q, r with | N0, N0 => (0%N, 0%N) | N0, Npos r => if (xO r) ?< b then (0%N, Npos (xO r)) else (1%N,PminusN (xO r) b) | Npos q, N0 => (Npos (xO q), 0%N) | Npos q, Npos r => if (xO r) ?< b then (Npos (xO q), Npos (xO r)) else (Npos (xI q),PminusN (xO r) b) end | xI a' => let (q, r) := div_eucl a' b in match q, r with | N0, N0 => (0%N, 0%N) | N0, Npos r => if (xI r) ?< b then (0%N, Npos (xI r)) else (1%N,PminusN (xI r) b) | Npos q, N0 => if 1 ?< b then (Npos (xO q), 1%N) else (Npos (xI q), 0%N) | Npos q, Npos r => if (xI r) ?< b then (Npos (xO q), Npos (xI r)) else (Npos (xI q),PminusN (xI r) b) end end.
imports: ZArith Lia ZCmisc