aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--theories/Arith/Div2.v7
1 files changed, 0 insertions, 7 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 202e7a97a8..f5e7ebb34b 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -118,13 +118,6 @@ Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
Intro H. Inversion H. Inversion H1.
Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
-(*
-Simpl. Rewrite <- plus_n_Sm. Auto with arith.
-Simpl. Rewrite <- plus_n_Sm. Intro H. Injection H. Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite <- plus_n_Sm. Auto with arith.
-Simpl. Rewrite <- plus_n_Sm. Intro H. Injection H. Auto with arith.
-*)
Qed.