proposition: Lemma algebraic_rt_closure: forall A (j' j : X A A), 1 <== j' -> j' * j' <== j' -> j<==j' -> j# <== j'.
proof: Proof. intros A j' j Hr Ht H. transitivity (j'#); auto with algebra. apply star_destruct_left_one. semiring_normalize. rewrite Ht, Hr. auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(Utils_WF) Coq(Relations) Coq(Eqdep_dec)