proposition: Theorem kleene_star_eq a b : a ^* * b = a * (a ^* * b) + b.
proof: Proof. by rewrite mulrA -plusSr -{3}(mul1r b) -mulrDl kleeneSr addrC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice