proposition: Lemma predn_exp m k : (m ^ k).-1 = m.-1 * (\sum_(i < k) m ^ i).
proof: Proof. rewrite -!subn1 -[in LHS](exp1n k) subn_exp; congr (_ * _). symmetry; rewrite (reindex_inj rev_ord_inj); apply: eq_bigr => i _ /=. by rewrite -subn1 -subnDA exp1n muln1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)