proposition: Lemma div_kleene a b : a / b ^* = (a / b ^*)%D * b ^*.
proof: Proof. apply/le_anti/andP; split; last first. - by rewrite -mul_div_equiv -mulrA kleene_sqr div_mul_le. - apply: set_join_le_ub => x /=. rewrite mul_div_equiv => Hx. apply: (le_trans Hx). 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