Mercurial > cpdt > repo

comparison src/Predicates.v @ 54:31622083ad5d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Spell-check
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Sep 2008 13:13:26 -0400
parents 422865e240b1
children 8d7a97b3bb91
comparison
equal deleted inserted replaced
53:422865e240b1 54:31622083ad5d
668 Abort. 668 Abort.
669 669
670 Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False. 670 Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False.
671 induction 1; crush. 671 induction 1; crush.
672 672
673 (** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero. Only one of these cases has any trickyness to it. *) 673 (** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero. Only one of these cases has any trickiness to it. *)
674 destruct n; destruct n0; crush. 674 destruct n; destruct n0; crush.
675 675
676 (** [[ 676 (** [[
677 677
678 n : nat 678 n : nat