theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
apply nat_elim2
[intro.reflexivity
- |intro.simplify.auto
+ |intro.simplify.autobatch
|intros.simplify.assumption
]
qed.
apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
intros.simplify.reflexivity.
intros.apply False_ind.
-apply not_le_Sn_O.
-goal 13.apply H.
+apply not_le_Sn_O;
+[2: apply H | skip].
intros.
simplify.apply H.apply le_S_S_to_le. apply H1.
qed.
apply nat_elim2
[intros.apply False_ind.apply (not_le_Sn_O ? H)
|intros.rewrite < minus_n_O.
- auto
+ autobatch
|intros.
generalize in match H2.
apply (nat_case n1)
rewrite > eq_minus_S_pred.
apply lt_pred
[unfold lt.apply le_plus_to_minus_r.applyS H1
- |apply H[auto|assumption]
+ |apply H[autobatch|assumption]
]
]
qed.
apply H.apply H1.
qed.
+theorem lt_O_minus_to_lt: \forall a,b:nat.
+O \lt b-a \to a \lt b.
+intros.
+rewrite > (plus_n_O a).
+rewrite > (sym_plus a O).
+apply (lt_minus_to_plus O a b).
+assumption.
+qed.
+
theorem distributive_times_minus: distributive nat times minus.
unfold distributive.
intros.