proposition: Lemma kleene_monotony a b : a <= b -> a ^* <= b ^*.
proof: Proof. move=> Hab. apply: set_add_led_set => k. have Hyp : forall i, a ^ i <= b ^ i. elim=> [|i IHi]. - by rewrite exp0. - by rewrite !expS; apply: led_mul. elim: k => [|k IHk]. - by rewrite set_add0 le0d. - rewrite !set_addS; exact: led_add. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice