fact: Fixpoint gcdn (n : nat) (a b : positive) : positive := match n with | O => 1 | S n => match a,b with | 1, _ => 1 | _, 1 => 1 | a~0, b~0 => (gcdn n a b)~0 | _ , b~0 => gcdn n a b | a~0, _ => gcdn n a b | a'~1, b'~1 => match a' ?= b' with | Eq => a | Lt => gcdn n (b'-a') a | Gt => gcdn n (a'-b') b end end end.
imports: BinNums