proposition: Lemma plusSr a : a ^+ = a * a ^*.
proof: Proof. rewrite set_mulDl /op_plus /op_kleene. apply: f_equal; rewrite predeqP => b; split. - by move=> [i _ <-]; rewrite expS; exists (a ^ i); [exists i|]. - by move=> [c [i _ <-] <-]; rewrite -expS; exists i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice