-theorem nle_inv_succ_2: \forall y,x. x <= succ y \to
- x = zero \lor \exists z. x = succ z \land z <= y.
- intros 2; elim x; clear x; intros;
- [ auto
- | lapply linear nle_inv_succ_succ to H1.
- 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.