proposition: Lemma mx_star_destruct_right: forall n m (M: MX n n) (Y: MX m n), Y*M <== Y -> Y*M# <== Y.
proof: Proof. induction n; intros. mx_intros i j Hi Hj. unfold star, mx_Star_Op. Opaque one dot plus leq. simpl. Transparent one dot plus leq. change (S n) with (1+n)%nat. apply build_star_destruct_right; trivial. clear - KA. intros m M Y H; mx_intros i j Hi Hj. unfold mx_of_scal. simpl. rewrite plus_neutral_right. apply star_destruct_right. specialize (H i O Hi (le_n _)). simpl in H. rewrite plus_neutral_right in H. assumption. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing)