proposition: Lemma modn_coprime k n : 0 < k -> (exists u, (k * u) %% n = 1) -> coprime k n.
proof: Proof. move=> k_gt0 [u Hu]; apply/coprimeP=> //. by exists (u, k * u %/ n); rewrite /= mulnC {1}(divn_eq (k * u) n) addKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)