Read about our upcoming Code of Conduct on this issue

Commit 6e519876 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

another broken proof

parent 3b2637ae2d8c
......@@ -153,9 +153,7 @@ lemma aadd_two_negg[simp]:"\<lbrakk>a < (0::ant); b < 0\<rbrakk> \<Longrightarro
by auto
lemma amin_aminTr:"(z::ant) \<le> z' \<Longrightarrow> amin z w \<le> amin z' w"
by (simp add:amin_def, simp add:aneg_le,
(rule impI)+, frule aless_le_trans[of "w" "z" "z'"],
assumption+, simp)
by (simp add:amin_def)
lemma amin_le1:"(z::ant) \<le> z' \<Longrightarrow> (amin z w) \<le> z'"
by (simp add:amin_def, simp add:aneg_le,
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment