Changeset 230 for Deliverables/D4.1/Matita/Nat.ma
 Timestamp:
 Nov 10, 2010, 5:26:08 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Nat.ma
r228 r230 108 108 nqed. 109 109 110 nlemma multiplication_zero :110 nlemma multiplication_zero_right_neutral: 111 111 ∀m: Nat. 112 112 m * Z = Z. … … 151 151 napplyS multiplication_succ. 152 152 nqed. 153 153 154 nlemma multiplication_succ_zero_left_neutral: 155 ∀m: Nat. 156 (S Z) * m = m. 157 #m. 158 nelim m. 159 nnormalize. 160 @. 161 #N H. 162 nnormalize. 163 napplyS succ_plus. 164 nqed. 165 166 nlemma multiplication_succ_zero_right_neutral: 167 ∀m: Nat. 168 m * (S Z) = m. 169 #m. 170 nelim m. 171 nnormalize. 172 @. 173 #N H. 174 nnormalize. 175 nrewrite > H. 176 @. 177 nqed. 178 179 nlemma multiplication_distributes_right_plus: 180 ∀m, n, o: Nat. 181 (m + n) * o = m * o + n * o. 182 #m n o. 183 nelim m. 184 nnormalize. 185 @. 186 #N H. 187 nnormalize. 188 nrewrite > H. 189 napplyS plus_associative. 190 nqed. 191 192 nlemma multiplication_distributes_left_plus: 193 ∀m, n, o: Nat. 194 o * (m + n) = o * m + o * n. 195 #m n o. 196 napplyS multiplication_symmetrical. 197 nqed. 198 199 nlemma mutliplication_associative: 200 ∀m, n, o: Nat. 201 m * (n * o) = (m * n) * o. 202 #m n o. 203 nelim m. 204 nnormalize. 205 @. 206 #N H. 207 nnormalize. 208 nrewrite > H. 209 napplyS multiplication_distributes_right_plus. 210 nqed. 211 212 nlemma minus_minus: 213 ∀n: Nat. 214 n  n = Z. 215 #n. 216 nelim n. 217 nnormalize. 218 @. 219 #N H. 220 nnormalize. 221 nrewrite > H. 222 @. 223 nqed. 224 225 (* 226 nlemma succ_injective: 227 ∀m, n: Nat. 228 S m = S n → m = n. 229 #m n. 230 nelim m. 231 #H. 232 ninversion H. 233 #H. 234 ndestruct 235 236 nlemma plus_minus_associate: 237 ∀m, n, o: Nat. 238 (m + n)  o = m + (n  o). 239 #m n o. 240 nelim m. 241 nnormalize. 242 @. 243 #N H. 244 245 246 nlemma plus_minus_inverses: 247 ∀m, n: Nat. 248 (m + n)  n = m. 249 #m n. 250 nelim m. 251 nnormalize. 252 napply minus_minus. 253 #N H. 254 *)
Note: See TracChangeset
for help on using the changeset viewer.