proposition: Lemma kapWP a b c : let: (p,q) := kap a b c in coprimer (p * a) (p * b + q * c) -> let: (x,y) := kapW a b c in x * (p * a) + y * (p * b + q * c) = 1.
proof: Proof. rewrite /kapW; case: kap => p q. case: coprimerP=> // [[[x y]]] /= Hxy _. by case: sig_eqW=> /= [[]]. Qed.
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