proposition: Lemma str_unique `{laws} `{STR ≪ l} n (a x: X n n): 1 ≦x -> a⋅x ≦ x -> (forall y: X n n, a⋅y ≦y -> x⋅y ≦y) -> a^* ≡ x.
proof: Proof. intros H1 H2 H3. apply antisym. now apply str_ind_l1. rewrite <-(dotx1 x), (str_refl a). apply H3. apply str_cons. Qed.
imports: monoid