include "classes/defs.ma".
theorem p_inv_O: P 0 → False.
- intros; inversion H; clear H; intros;
- [ destruct
- | lapply linear plus_inv_O3 to H3; decompose; destruct;
- autobatch depth = 2
- ].
+ intros; inversion H;intros;
+ [apply (not_eq_O_S ? H1)
+ |autobatch.
+ ]
qed.
theorem t_inv_O: T 0 → False.
qed.
theorem p_pos: ∀i. P i → ∃k. i = S k.
- intros 1; elim i names 0; clear i; intros;
+ intros 1; elim i 0; clear i; intros;
[ lapply linear p_inv_O to H; decompose
| autobatch depth = 2
].