proposition: Lemma mul_kleene a b : a * b ^* = (a * b ^*) / b ^*.
proof: Proof. apply/le_anti/andP; split. - by rewrite -mul_div_equiv -mulrA kleene_sqr. - apply: set_join_le_ub => x. apply: le_trans. by rewrite kleeneSr mulrDr mulr1 led_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice