proposition: Lemma kleene_add_mul a b : (a + b) ^* = a ^* * b ^*.
proof: Proof. apply/le_anti/andP; split. - apply: set_join_le_ub => _ [i _ <-]. elim: i => [ | i IHi]. + rewrite exp0 -(mulr1 1%R). apply: led_mul. * rewrite kleeneSr -{1}(addr0 1%R). exact/led_add2l/le0d. * rewrite kleeneSr -{1}(addr0 1%R). exact/led_add2l/le0d. + rewrite expS. apply: (le_trans (led_mul2l _ IHi)). rewrite mulrDl mulrA -plusSr (mulrC b) -mulrA -(mulrC b) -plusSr. rewrite !kleeneSr !mulrDl !mulrDr !mulr1 !mul1r. rewrite !addrA (addrC (a^+)) addrC !addrA adddd. rewrite [X in _ <= X]addrC -!addrA (addrC 1%R) (addrC (a^+)) !addrA. exact: led_addr. - rewrite {2}/op_kleene set_mulDl. apply: set_join_le_ub => _ [_ [i _ <-] <-]. rewrite {1}/op_kleene set_mulDr. apply: set_join_le_ub => _ [_ [j _ <-] <-]. elim: i => [ | i HIi]. + rewrite exp0 mulr1. elim: j => [ | j HIj]; [by rewrite exp0 kleeneSr led_addr|]. rewrite expS kleeneSr plusSr -(add0r (_ * _)). apply: led_add; [exact: le0d|]. apply: led_mul => [ | //]. exact: led_addr. + rewrite expS (mulrC b) mulrA. apply: (le_trans (led_mul2r _ HIi)). rewrite mulrC {2}kleeneSr plusSr -(add0r (_ * _)). apply: led_add; [exact: le0d|]. exact/led_mul2r/led_addl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice