## 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 |

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). |