Handle fractions in denominators

This should deal with #16 /
https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009776

1 files changed, 3 insertions, 8 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 81d1b102b..c0f3b1fba 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -732,15 +732,10 @@ Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac con
   | appcontext[div]
     => lazymatch T with
        | div ?numerator ?denominator
-         => let d := fresh "d" in
-            pose denominator as d;
-            cut (not (eq d zero));
+         => cut (not (eq denominator zero));
             [ intro;
-              set_nonfraction_pieces_on
-                numerator eq zero opp add sub mul inv div nonzero_tac
-                ltac:(fun numerator'
-                      => cont (div numerator' d))
-            | subst d; nonzero_tac ]
+              two_arg_recr div numerator denominator
+            | nonzero_tac ]
        | opp ?x => one_arg_recr opp x
        | inv ?x => one_arg_recr inv x
        | add ?x ?y => two_arg_recr add x y