proposition: Lemma kleene_1r a : (a + 1) ^* = a ^*.
proof: Proof. apply/le_anti/andP; split; [|exact/kleene_monotony/led_addr]. suff Hyp : forall i, (a + 1) ^ i = set_add [set a ^ j | j in [set x | 'I_i.+1 x]]. { apply: set_add_led_set => k. elim: k => [ | k IHk]; [by rewrite set_add0 le0d|]. rewrite !set_addS Hyp. rewrite -[in X in _ <= X](adddd (set_add _)) -addrA. apply: (led_add IHk). by rewrite set_addS. } elim=> [ | i IHi]; [by rewrite set_add1 !exp0|]. rewrite expS mulrDl mul1r IHi set_mulDl. set B' := [set a ^ j | j in [set j | (1 <= j <= i)%N]]. rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B'); last first. { rewrite predeqP => x; split. - move=> -[y [[j Hj] _ <-] <-]. rewrite expS /= -!expS. move: Hj; rewrite leq_eqVlt ltnS => /orP[/eqP [->] | Hj]; [by left|]. by right; exists j.+1. - move=> [->|]; [by rewrite expS; exists (a ^ i) => //; exists ord_max|]. move=> -[[//|j] /andP [Hj Hji] <-]; rewrite expS; exists (a ^ j) => //. by move: Hji => /ltnW; rewrite -ltnS => Hji; exists (Ordinal Hji). } rewrite -[set_join]/set_add set_addDl. rewrite (_ : image _ _ = (1%R |` B')); last first. { rewrite predeqP => x; split. { move=> -[[[|j] Hj] _ <-]; [by left; rewrite exp0|]. by right; exists (Ordinal Hj). } move=> [-> | [j /= Hj <-]]; [by rewrite -(exp0 a); exists ord0|]. by move: Hj => /andP[_]; rewrite -ltnS => Hj; exists (Ordinal Hj). } rewrite set_addDl. rewrite (addrC (a ^ 0)) addrA -(addrA (a ^ i.+1)) adddd addrC -!set_addDl. apply: f_equal; rewrite predeqP => x; split. - move=> [-> | [-> | [j /= Hj <-]]]. + by exists ord0. + by exists ord_max. + move: Hj => /andP[_]; rewrite -ltnS; move=> /ltnW; rewrite -ltnS => Hj. by exists (Ordinal Hj). - move=> -[[[|j] Hj] _ <-]; [by left|right]. move: Hj; rewrite /nat_of_ord !ltnS leq_eqVlt => /orP[/eqP -> | ]; [by left|]. by rewrite -ltnS => Hj; right; exists (Ordinal Hj). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice