proposition: Lemma kleene_mul_expl a n : a ^ n * a ^* <= a^*.
proof: Proof. elim: n => [|n IHn]; [by rewrite mul1r|]. rewrite expSr -mulrA. move: IHn; apply/le_trans/led_mul2l. rewrite -plusSr; apply: plus_le_kleene. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice