proposition: Lemma le_plus a : a <= a ^+.
proof: Proof. by rewrite le_def plusSr kleeneSr mulrDr mulr1 addrA adddd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice