Garside divisibility and lcm assertions for A+

[F1] For a spherical Artin system, the positive submonoid $A^{+}$ is a Garside monoid and its left and right divisibility orders have gcds and lcms for every pair. (Independent spherical Artin Garside input)

[F2] For every $I\subseteq {\mathrm{\Gamma }}_0$ and $a\in I^c$, the elementary ribbon ${\mu }_{a,I}$ belongs to $A^{+}$. (Positive elementary ribbon elements)

[F3] In a monoid, $x$ left-divides $y$ when $y=xz$ for some monoid element $z$; right divisibility reverses the side of the factor. A gcd is a greatest common divisor and an lcm a least common multiple in the relevant divisibility order. The Garside interface uses these divisibility orders as lattices. (Categorical Garside structures and simple arrows)

[F4] The Coxeter diagram, its group $W$ and its indexed simple generators $S=\{s_i:i\in {\mathrm{\Gamma }}_0\}$ are supplied by Coxeter-system, roots, length and weak-order conventions. For finite $S$, Artin–Tits group, pure subgroup and positive lifts supplies the associated Artin–Tits group $A$ and its standard generators through a fixed isomorphism from the presented Artin group. The positive submonoid generated by these generators is the $A^{+}$ of Positive Artin and parabolic monoids.

Given: A spherical Coxeter diagram and its positive Artin submonoid $A^{+}$; for the final assertion, an associate $I$ of $J$ and $a,b\in I^c$.

Goal: Establish the Garside and divisibility assertions and the existence of the displayed left lcm.