diff options
Diffstat (limited to 'flocq/Appli/Fappli_rnd_odd.v')
| -rw-r--r-- | flocq/Appli/Fappli_rnd_odd.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v index b6d985ac..273c1000 100644 --- a/flocq/Appli/Fappli_rnd_odd.v +++ b/flocq/Appli/Fappli_rnd_odd.v @@ -199,7 +199,7 @@ case (Zeven (Zfloor r)); simpl; ring. apply trans_eq with (Zeven (Zceil r)). rewrite Zceil_floor_neq. rewrite Zeven_plus. -simpl; reflexivity. +destruct (Zeven (Zfloor r)); reflexivity. now apply sym_not_eq. rewrite <- (Zeven_opp (Zfloor (- r))). reflexivity. |