diff options
| -rw-r--r-- | src/Util/ZUtil.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index b87c20b79..30cb38857 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -759,11 +759,19 @@ Module Z. Ltac pre_reorder_fractions_step := match goal with | [ |- context[?x / ?y * ?z] ] - => rewrite (Z.mul_comm (x / y) z) + => lazymatch z with + | context[_ / _] => fail + | _ => idtac + end; + rewrite (Z.mul_comm (x / y) z) | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in match LHS with | context G[?x * (?y / ?z)] - => let G' := context G[(x * y) / z] in + => lazymatch x with + | context[_ / _] => fail + | _ => idtac + end; + let G' := context G[(x * y) / z] in transitivity G' end end. |