theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
intros 2; elim y; clear y;
- [ auto
+ [ auto new timeout=100
| decompose;
[ lapply linear nle_gen_succ_1 to H1. decompose.
- rewrite > H1. clear H1 n. auto
+ subst. auto new timeout=100 depth=4
| lapply linear nle_lt_or_eq to H1; decompose;
- [ auto
- | rewrite > H. clear H n. auto
- ]
+ subst; auto new timeout=100
]
].
qed.