-theorem nle_trans: \forall x,y. x <= y \to
- \forall z. y <= z \to x <= z.
- intros 3. elim H; clear H x y;
- [ auto
- | lapply linear nle_inv_succ_1 to H3. decompose. subst.
- auto
+theorem nle_trans: ∀x,y. x ≤ y → ∀z. y ≤ z → x ≤ z.
+ intros 3; elim H; clear H x y;
+ [ autobatch
+ | lapply linear nle_inv_succ_1 to H3. decompose. destruct.
+ autobatch