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