fact: Fixpoint egcd_log2 (a b c:positive) {struct c}: option (Z * Z * positive) := match a/b with | (_, N0) => Some (0, 1, b) | (q, Npos r) => match b/r, c with | (_, N0), _ => Some (1, -q, r) | (q', Npos r'), xH => None | (q', Npos r'), xO c' => match egcd_log2 r r' c' with None => None | Some (u', v', w') => let u := u' - v' * q' in Some (u, v' - q * u, w') end | (q', Npos r'), xI c' => match egcd_log2 r r' c' with None => None | Some (u', v', w') => let u := u' - v' * q' in Some (u, v' - q * u, w') end end end.
imports: ZArith Lia ZCmisc