The Coq mailing list

[Brian Huffman <brianh AT cs.pdx.edu>]

On Mon, Aug 1, 2011 at 8:16 PM, S3 
<scubed2 AT gmail.com>
 wrote:
> Start with a simple definition for divides evenly:
[...]
> Inductive divides: nat -> nat -> Prop :=
>  | divides_0 n: divides 0 n
>  | divides_n n m: divides n m -> divides (n + m) m
> .
[...]
> But, how would I prove that:
> forall n, divides (S n) 0 -> False.

I managed to prove this by proving a related lemma first:

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

Formulated this way, divides_zero can be proved by a straightforward
induction on the "divides" predicate.

Your original goal, "forall n, divides (S n) 0 -> False" can be
derived fairly directly from divides_zero.

- Brian