proposition: Lemma modp_coprime k u n : k != 0 -> (k * u) %% n %= 1 -> coprimep k n.
proof: Proof. move=> kn0 hmod; apply/Bezout_coprimepP. exists (((lead_coef n)^+(scalp (k * u) n) *: u), (- (k * u %/ n))). rewrite -scalerAl mulrC (divp_eq (u * k) n) mulNr -addrAC subrr add0r. by rewrite mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)