fact: Definition gdco_kap (a b c : R) : R * R := let: (_, x, y, z, _, _, _) := egcdr3 a b c in if a == 0 then (y, z) else let: r := gdco c a in let: (g, _, v, _, _) := egcdr r c in if (1 - b) %/? g is Some k' then (1, k' * v) else (1, 0).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr