proposition: Lemma expS i a : a ^ (i.+1) = a * (a ^ i).
proof: Proof. by case: i => //; rewrite exp0 mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice