-theorem plus_inv_S_S_S: \forall x,y,z. S x = S y + S z \to S y <= x \land S z <= x.
- simplify; intros; destruct;
- rewrite < plus_n_Sm in \vdash (? (? ? %) ?); autobatch depth = 3.
+theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
+ simplify; intros; destruct;autobatch.