proposition: Lemma kleene_sqr a : a^* * a^* = a^*.
proof: Proof. rewrite {1}/op_kleene set_mulDr. set B' := (a ^* |` (range (fun i => a ^ i.+1 * a ^*))). rewrite (_ : image _ _ = B'); last first. { rewrite predeqP => x; split. - by move=> -[_ [[|i] _ <-] <-]; [left; rewrite exp0 mul1r|right; exists i]. - move=> [-> | [i _ <-]]; [by exists 1%R; [exists O|rewrite mul1r]|]. by exists (a ^ i.+1); [exists i.+1|]. } rewrite -[set_join]/set_add set_addDl. apply/eqP; rewrite addrC -le_def; apply: set_add_lim_nat. elim=> [|k]. - by rewrite (set_add0 (fun i => a ^ i.+1 * _)) le0d. - rewrite (set_addS (fun i => a ^ i.+1 * _)). rewrite !le_def => /eqP IHk. rewrite addrAC IHk addrC -le_def. exact: kleene_mul_expl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice