proposition: Lemma star_mon_is_one (a: X A A): a <== 1 -> a# == 1.
proof: Proof. intro H. apply leq_antisym. star_left_induction. rewrite H; semiring_reflexivity. apply one_leq_star_a. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing)