proposition: Theorem kleene_star_least a b : forall x, (x = a * x + b) -> a ^* * b <= x.
proof: Proof. move=> x Hx. rewrite set_mulDr. rewrite [X in set_join X](_ : _ = [set (a ^ i) * b | i in setT]); last first. rewrite predeqP => y; split. - by move=> [_ [i _ <-] <-]; exists i. - by move=> [i _ <-]; exists (a ^ i); [exists i|]. apply: set_add_lim_nat; elim=> [ | k IHk]. by rewrite le_def (set_add0 (fun i => a ^ i * b)) add0r. rewrite (set_addS (fun i => a ^ i * b)) led_addE IHk /=. elim: k {IHk} => [ | k IHk]; [by rewrite mul1r Hx led_addl|]. rewrite expS. have Ha : a * x <= x; [by rewrite {2}Hx led_addr|]. by apply: (le_trans _ Ha); rewrite -mulrA led_mul2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice