Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Lemma assoc_a :
- forall a b c d : nat,
- ((a + b) + c) + d = a + (b + (c + d)).
- Proof.
- intros a b c d.
- rewrite -> (plus_assoc a b (c + d)).
- rewrite -> (plus_assoc (a + b) c d).
- reflexivity.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement