Mercurial > cpdt > repo

comparison src/LogicProg.v @ 540:582bf8d4ce51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fuller English fix
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Aug 2015 15:59:02 -0400
parents 8dddcaaeb67a
children 1dc1d41620b6
comparison
equal deleted inserted replaced
539:8dddcaaeb67a 540:582bf8d4ce51
775 crush. 775 crush.
776 Qed. 776 Qed.
777 777
778 Hint Resolve plus_0 times_1. 778 Hint Resolve plus_0 times_1.
779 779
780 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) 780 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _semiring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
781 781
782 Require Import Arith Ring. 782 Require Import Arith Ring.
783 783
784 Theorem combine : forall x k1 k2 n1 n2, 784 Theorem combine : forall x k1 k2 n1 n2,
785 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2). 785 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).