proposition: Lemma kleene_kleene a : (a ^*) ^* = a ^*.
proof: Proof. rewrite kleeneSr /op_plus. rewrite (_ : image _ _ = a ^* |` set0). by rewrite setU0 set_join1 kleeneSr addrA adddd. rewrite predeqP => x; split. - move=> [i _ <-]; left; exact: kleene_exp. - by move=> [-> | //]; exists O. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice