proposition: Lemma kleene_div_equiv a : (a == a ^*) = (a == a / a).
proof: Proof. apply/idP/idP => /eqP. - move=> ->. apply/eqP/le_anti/andP; split. + apply: set_join_le_ub => _ [i _ <-]. rewrite -mul_div_equiv. exact: kleene_mul_expl. + apply: set_join_le_ub => x /=. rewrite {1}kleeneSr mulrDr mulr1. by rewrite led_addE => /andP[]. - move=> Ha; apply/eqP/le_anti/andP; split; [exact: le_kleene|]. apply: set_join_le_ub => _ [i _ <-]. elim: i => [ | i IHi]; [by rewrite exp0 Ha -mul_div_equiv mul1r|]. by rewrite expSr mul_div_equiv -Ha. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice