Conservative definition
Parameters: a, b
exists h. h + a = bDefinition prerequisites
Theorem uses (notation, not proof premises)
AP001 · AP002 · AP004 · AP006 · AP007 · AP008 · AP009 · AP010 · AP011 · AP012 · AP013 · AP014 · AP015 · AP016 · AP017 · AP021 · AP023 · AP024 · AP031 · AP032 · AP033 · AP034 · AP035 · AP036 · AP037 · AP039 · AP040 · AP041 · AP042 · AP043 · AP044 · AP045 · AP046 · AP047 · AP048 · AP049 · AP050 · AP051 · AP052 · AP053 · AP054 · AP055 · AP056 · AP057 · AP058 · AP059 · AP061 · AP062 · AP063 · AP064 · AP065 · AP066 · AP067 · AP068 · AP069 · AP070 · AP071 · AP072 · AP073 · AP074 · AP075 · AP076 · AP077 · AP079 · AP080 · AP081 · AP082 · AP083 · AP084 · AP085 · AP086 · AP087 · AP088 · AP089 · AP090 · AP091 · AP092 · AP093 · AP094 · AP095 · CV005 · CV022 · CV023 · CV024 · CV028 · CV029 · CV030 · CV031 · CV032 · CV034 · CV038 · CV039 · CV040 · CV041 · CV051 · CV052 · CV054 · CV055 · CV056 · CV057 · CV058 · CV061 · CV063 · CV064 · CV065 · CV066 · CV067 · CV068 · CV070 · CV071 · CV074 · CV075 · CV076 · CV077 · CV078 · CV079 · CV080 · CV081 · CV083 · CV084 · CV085 · CV086 · CV087 · CV088 · CV089 · CV090 · CV094 · CV095 · CV096 · CV098 · CV099 · CV100 · CV101 · CV102 · SQ002 · SQ003 · SQ004 · SQ005 · SQ006 · SQ008 · SQ009 · SQ010