proposition: Lemma le_kleene a : a <= a^*.
proof: Proof. exact/(le_trans (le_plus a))/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