(* This code is copyrighted by its authors; it is distributed under  *)
(* the terms of the LGPL license (see LICENSE and description files) *)

 Load "hMinus".

Notation spminusf1 :=
  (spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec)
  (only parsing).

