Lemma cpoly_C_ : forall c : R[x], _C_ c [=] c[+X*]0.
algebra.
Qed.
has a mistake in it.
The statement ought to read forall c : R, _C_ c [=] c[+X*]0.
It is no problem to fix it. I only point this out because it is
interesting to find mistakes in computer verified theorems. No one
directly uses this lemma (but it is part of a hint database), so no one
noticed this mistake before.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
_______________________________________________
C-CoRN mailing list
[email protected]
http://mailman.science.ru.nl/mailman/listinfo/c-corn
