The Coq mailing list

[S3 <scubed2 AT gmail.com>]

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

Start with a simple definition for divides evenly:
(Note: I know the arguments are usually written
the other way around.  I arbitrarily decided to write
it in normal division operator order.)

Inductive divides: nat -> nat -> Prop :=
  | divides_0 n: divides 0 n
  | divides_n n m: divides n m -> divides (n + m) m
.

So, with this definition,
divides 0 0.
forall n, divides n 1.
forall n m, divides (n*m) n.
And those can all be easily and directly proven.

But, how would I prove that:
forall n, divides (S n) 0 -> False.
Normally, I would just use inversion,
but in this case, the predecessor is itself,
forming a cycle.  What technique do you use
when you form a cycle?

- -- 
main(){char s[]="+~{Y$-:>2vp5z^",c=244,i;int j=44404;
for(;j>0;j--)for(i=0;i<14;i++)c+=s[i]-=c;puts(s);}
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Gentoo - http://enigmail.mozdev.org/

iEYEARECAAYFAk414qwACgkQxzVgPqtIcfve+QCfaNJnCEn4g7661zi3Yi7ckk2T
MrkAn1Zf0Yze60CNgZLko0O9UtLTuMA1
=jQuI
-----END PGP SIGNATURE-----