| (pos m) \Rightarrow
match y with
[ OZ \Rightarrow x
- | (pos n) \Rightarrow (pos (S (m+n)))
+ | (pos n) \Rightarrow (pos (pred ((S m)+(S n))))
| (neg n) \Rightarrow
match nat_compare m n with
[ LT \Rightarrow (neg (pred (n-m)))
[ LT \Rightarrow (pos (pred (n-m)))
| EQ \Rightarrow OZ
| GT \Rightarrow (neg (pred (m-n)))]
- | (neg n) \Rightarrow (neg (S (m+n)))]].
+ | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]].
(*CSC: the URI must disappear: there is a bug now *)
interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).
intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
elim y.simplify.reflexivity.
simplify.
-rewrite < sym_plus.reflexivity.
+rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
simplify.
rewrite > nat_compare_n_m_m_n.
simplify.elim nat_compare ? ?.simplify.reflexivity.
simplify.elim nat_compare ? ?.simplify.reflexivity.
simplify. reflexivity.
simplify. reflexivity.
-simplify.rewrite < sym_plus.reflexivity.
+simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
qed.
theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
simplify.reflexivity.
simplify.reflexivity.
elim m.
-simplify.
+simplify.rewrite < plus_n_Sm.
rewrite < plus_n_O.reflexivity.
-simplify.
+simplify.rewrite < plus_n_Sm.
rewrite < plus_n_Sm.reflexivity.
qed.
simplify.reflexivity.
simplify.reflexivity.
elim m.
-simplify.rewrite < plus_n_Sm.reflexivity.
+simplify.rewrite > plus_n_Sm.reflexivity.
simplify.rewrite > plus_n_Sm.reflexivity.
qed.