include "Coq.ma".
-(*#**********************************************************************)
-
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-
-(* \VV/ *************************************************************)
-
-(* // * This file is distributed under the terms of the *)
-
-(* * GNU Lesser General Public License Version 2.1 *)
-
-(*#**********************************************************************)
-
include "Num/Axioms.ma".
include "Num/EqAxioms.ma".
-(*#* This file contains basic properties of addition with respect to equality *)
-
-(*#* Properties of Addition *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_0.con ******************)
inline procedural "cic:/Coq/Num/AddProps/add_x_0.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_0 : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_Sy.con *****************)
inline procedural "cic:/Coq/Num/AddProps/add_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_Sy_swap.con ************)
inline procedural "cic:/Coq/Num/AddProps/add_x_Sy_swap.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_Sy_swap : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_Sx_y_swap.con ************)
inline procedural "cic:/Coq/Num/AddProps/add_Sx_y_swap.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_Sx_y_swap : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_assoc_r.con **************)
inline procedural "cic:/Coq/Num/AddProps/add_assoc_r.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_assoc_r : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_y_z_perm.con ***********)
inline procedural "cic:/Coq/Num/AddProps/add_x_y_z_perm.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_y_z_perm : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_x_one_S.con **************)
inline procedural "cic:/Coq/Num/AddProps/add_x_one_S.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_x_one_S : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/AddProps/add_one_x_S.con **************)
inline procedural "cic:/Coq/Num/AddProps/add_one_x_S.con" as lemma.
-(* UNEXPORTED
-Hints Resolve add_one_x_S : num.
-*)
-