proposition: Lemma expSr i a : a ^ i.+1 = a ^ i * a.
proof: Proof. elim: i => [ | i Hi]; first by rewrite exp0 mul1r. by rewrite expS {1}Hi expS mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice