chore(theories/number_theory/dioph): cleanup

leanprover-community · Dec 5, 2017 · b1981c9 · b1981c9
1 parent 7191e39
commit b1981c9
Show file tree

Hide file tree

Showing 2 changed files with 44 additions and 284 deletions.
diff --git a/data/int/basic.lean b/data/int/basic.lean
@@ -526,7 +526,7 @@ end
 
 /- nat abs -/
 
-attribute [simp] nat_abs
+attribute [simp] nat_abs nat_abs_of_nat nat_abs_zero nat_abs_one
 
 theorem nat_abs_add_le (a b : ℤ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b :=
 begin