Skip to content
Snippets Groups Projects
Commit 05b62d19 authored by Ralf Jung's avatar Ralf Jung
Browse files

make Z_local_update statement more intuitive

parent b990ffb7
No related branches found
No related tags found
No related merge requests found
......@@ -222,7 +222,7 @@ Section Z.
Proof. by intros ???? ?%Z.add_cancel_l. Qed.
Lemma Z_local_update (x y x' y' : Z) :
x + y' = x' + y (x,y) ~l~> (x',y').
x - y = x' - y' (x,y) ~l~> (x',y').
Proof.
intros. rewrite local_update_unital_discrete=> z _.
compute -[Z.sub Z.add]; lia.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment