1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/RELATIONAL/NLE/dec".
17 include "NLE/props.ma".
19 theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
20 intros 2; elim y; clear y;
21 [ auto new timeout=100
23 [ lapply linear nle_gen_succ_1 to H1. decompose.
24 subst. auto new timeout=100 depth=4
25 | lapply linear nle_lt_or_eq to H1; decompose;
26 subst; auto new timeout=100