(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/nat".
+set "baseuri" "cic:/matita/library_autobatch/nat/nat".
include "higher_order_defs/functions.ma".
| (S p) \Rightarrow p ].
theorem pred_Sn : \forall n:nat.n=(pred (S n)).
- auto.
+ autobatch.
(*intros. reflexivity.*)
qed.
intros.
rewrite > pred_Sn.
rewrite > (pred_Sn y).
- auto.
+ autobatch.
(*apply eq_f.
assumption.*)
qed.
intros.
unfold Not.
intros.
- auto.
+ autobatch.
(*apply H.
apply injective_S.
assumption.*)
(n=O \to P O) \to (\forall m:nat. (n=(S m) \to P (S m))) \to P n.
intros 2;
elim n
- [ auto
+ [ autobatch
(*apply H;
reflexivity*)
- | auto
+ | autobatch
(*apply H2;
reflexivity*) ]
qed.
| apply (nat_case m)
[ apply H1
|intro;
- auto
+ autobatch
(*apply H2;
apply H3*)
]
intros.unfold decidable.
apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))))
[ intro; elim n1
- [auto
+ [autobatch
(*left;
reflexivity*)
- |auto
+ |autobatch
(*right;
apply not_eq_O_S*) ]
| intro;
right;
intro;
apply (not_eq_O_S n1);
- auto
+ autobatch
(*apply sym_eq;
assumption*)
| intros; elim H
- [ auto
+ [ autobatch
(*left;
apply eq_f;
assumption*)
| right;
intro;
- auto
+ autobatch
(*apply H1;
apply inj_S;
assumption*)