Unverified Commit d9e1175b authored by Maxime Dénès's avatar Maxime Dénès Committed by GitHub
Browse files

Simplify two scripts in Zbits (#369)

Previous scripts were relying on the order in which apply's HO
unification performs reductions, for a goal that could be solved by
reflexivity.
parent b6a7b8ee
......@@ -266,7 +266,7 @@ Qed.
Remark Ztestbit_shiftin_base:
forall b x, Z.testbit (Zshiftin b x) 0 = b.
Proof.
intros. rewrite Ztestbit_shiftin. apply zeq_true. omega.
intros. rewrite Ztestbit_shiftin; reflexivity.
Qed.
Remark Ztestbit_shiftin_succ:
......@@ -316,7 +316,7 @@ Qed.
Remark Ztestbit_base:
forall x, Z.testbit x 0 = Z.odd x.
Proof.
intros. rewrite Ztestbit_eq. apply zeq_true. omega.
intros. rewrite Ztestbit_eq; reflexivity.
Qed.
Remark Ztestbit_succ:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment