proposition: Lemma is_iexp1 (R : ringType) k s : is_iexp R k s 1.
proof: Proof. split=> [|c cR]; first by rewrite /coprime gcd1n. by apply: introspective1l. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound