fact: Fixpoint gcd_log2 (a b c:positive) {struct c}: option positive := match a mod b with | N0 => Some b | Npos r => match b mod r, c with | N0, _ => Some r | Npos r', xH => None | Npos r', xO c' => gcd_log2 r r' c' | Npos r', xI c' => gcd_log2 r r' c' end end.
imports: ZArith Lia ZCmisc