match nat_compare m n with
[ LT \Rightarrow (neg (pred (n-m)))
| EQ \Rightarrow OZ
- | GT \Rightarrow (pos (pred (m-n)))]]
+ | GT \Rightarrow (pos (pred (m-n)))] ]
| (neg m) \Rightarrow
match y with
[ OZ \Rightarrow x
[ LT \Rightarrow (pos (pred (n-m)))
| EQ \Rightarrow OZ
| GT \Rightarrow (neg (pred (m-n)))]
- | (neg n) \Rightarrow (neg (pred ((S m)+(S 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/plus/Zplus.con x y).