[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/library_autobatch/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (minus x y).
theorem minus_n_O: \forall n:nat.n=n-O.
intros.