Commit db356aa5 authored by Jason Gross's avatar Jason Gross

Don't depend on the judgmental behavior of Bool.eqb

This change is backwards compatible.
parent b5a7ee92
...@@ -199,7 +199,7 @@ case (Zeven (Zfloor r)); simpl; ring. ...@@ -199,7 +199,7 @@ case (Zeven (Zfloor r)); simpl; ring.
apply trans_eq with (Zeven (Zceil r)). apply trans_eq with (Zeven (Zceil r)).
rewrite Zceil_floor_neq. rewrite Zceil_floor_neq.
rewrite Zeven_plus. rewrite Zeven_plus.
simpl; reflexivity. destruct (Zeven (Zfloor r)); reflexivity.
now apply sym_not_eq. now apply sym_not_eq.
rewrite <- (Zeven_opp (Zfloor (- r))). rewrite <- (Zeven_opp (Zfloor (- r))).
reflexivity. reflexivity.
......
Markdown is supported
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