Re: [isabelle] simple lemma in ring theory

Dear Tao Ma,

blast is usually quite good at proving simple lemmas on divisibility, after unfolding the definition, of course. Here's a more concise version of your proof:

lemma (in "domain")
  assumes xr: "x \<in> carrier R"
  and yr:  "y \<in> carrier R"
  shows "dvd1 R x (x \<otimes> y)"
using xr and yr
by (unfold dvd1_def) blast


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.