proposition: Lemma kleene_exp a i : (1 <= i)%N -> (a ^*) ^ i = a ^*.
proof: Proof. case: i => [// | ] i _; elim: i => [// | i IHi]. by rewrite expS IHi kleene_sqr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice