The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

> Lemma divides_zero :
>   forall n m, divides n m -> m = 0 -> n = 0.

Thanks!  That work well and surprisingly easily.
My initial theorem is a direct corollary, as you stated.

It was interesting how minor variations of it didn't work.
(Unfortunately, I'm still a novice, so I don't quite
understand why the simpler form doesn't work.)

If I try a simpler form:
Theorem divides_only_0 n: divides n 0 -> n = 0.
inducting on divides gives a useless hypothesis.
I tried to be fancier and make it like the form you gave
by doing:
assert (exists m, m=0).
That seemed to work identically to your version.

So, the moral of the story is that I have to
additionally state explicitly that m is 0,
otherwise the induction doesn't know
if divides might zig-zag changing m.

- -- 
*********************.************************************..|
**..*.*...*..**....**....*....**....***.**...*..***.......*.|
*..**.**...**.***...*...*..*.**..****...*...*.*.....**..*...|
.*..*..*.*..*.....******...*.*..*.*.**...*.**.*..*..***..*..|
...*.*..*..***..*.*****...*...*....****.....***.*...**..**..|
..*.....**..***.*.........*.*...*..**..**game*.....*........|
*....*..**..*.*.*.*..*.**.*..*..*..**..**of**......**.***...|
*.**.*..**..*.*.**.**..**.**.****..***life.**.****..*.****..|
**********************************************************..|
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Gentoo - http://enigmail.mozdev.org/

iEYEARECAAYFAk43iCoACgkQxzVgPqtIcftq2gCfQoJpReoqiOZjLs7wmoyCQWVD
yvAAn2ti4YuDDYgHoZr4Yeq88lX9vfKN
=SPAg
-----END PGP SIGNATURE-----