fact: Definition kapW a b c : R * R := let: (p,q) := kap a b c in if coprimerP (p * a) (p * b + q * c) is ReflectT P then projT1 (sig_eqW P) else (0,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