-theorem nle_inv_succ_2: \forall y,x. x <= succ y \to
- x = zero \lor \exists z. x = succ z \land z <= y.
- intros. inversion H; clear H; intros; subst; auto depth = 4.
+theorem nle_inv_succ_2: ∀y,x. x ≤ succ y →
+ x = zero ∨ ∃z. x = succ z ∧ z ≤ y.
+ intros; inversion H; clear H; intros; destruct;
+ autobatch depth = 4.