Fix sqrt handling in specificgen

6 files changed, 186 insertions, 148 deletions

diff --git a/src/SpecificGen/GF2213_32Bounded.v b/src/SpecificGen/GF2213_32Bounded.v
index b5ffd40fd..c98f234a0 100644
--- a/src/SpecificGen/GF2213_32Bounded.v
+++ b/src/SpecificGen/GF2213_32Bounded.v
@@ -294,7 +294,6 @@ Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe2213_32W_word64ize word64ize andb o
 
 Definition GF2213_32sqrt (x : GF2213_32.fe2213_32) : GF2213_32.fe2213_32.
 Proof.
-Print GF2213_32.sqrt.
   lazymatch (eval cbv delta [GF2213_32.sqrt] in GF2213_32.sqrt) with
   | (fun powf powf_squared f => dlet a := powf in _)
     => exact (dlet powx := powW (fe2213_32ZToW x) (chain GF2213_32.sqrt_ec) in
@@ -314,39 +313,48 @@ Proof.
   split.
   { etransitivity.
     Focus 2. {
-      apply Proper_Let_In_nd_changebody_eq; intros;
-        set_evars;
-        match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
-        | [ |- ?x = dlet y := fe2213_32WToZ ?z in ?f ]
-          => is_var z; change (x = match fe2213_32WToZ z with y => f end)
-        end;
-        change sqrt_m1 with (fe2213_32WToZ sqrt_m1W);
-        rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe2213_32WToZ)
-          by repeat match goal with
-                    | _ => progress subst
-                    | [ |- is_bounded (fe2213_32WToZ ?op) = true ]
-                      => lazymatch op with
-                         | mulW _ _ => apply mulW_correct_and_bounded
-                         | mulW_noinline _ _ => apply mulW_correct_and_bounded
-                         | powW _ _ => apply powW_correct_and_bounded
-                         | sqrt_m1W => vm_compute; reflexivity
-                         | _ => assumption
-                         end
-                    end;
-        subst_evars; reflexivity.
+      lazymatch goal with
+      | [ |- _ = pow _ _ ]
+        => apply powW_correct_and_bounded; assumption
+      | [ |- _ = (dlet powx := _ in _) ]
+        => apply Proper_Let_In_nd_changebody_eq; intros;
+             set_evars;
+             match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
+             | [ |- ?x = dlet y := fe2213_32WToZ ?z in ?f ]
+               => is_var z; change (x = match fe2213_32WToZ z with y => f end)
+             end;
+             change sqrt_m1 with (fe2213_32WToZ sqrt_m1W);
+             rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe2213_32WToZ)
+               by repeat match goal with
+                         | _ => progress subst
+                         | [ |- is_bounded (fe2213_32WToZ ?op) = true ]
+                           => lazymatch op with
+                              | mulW _ _ => apply mulW_correct_and_bounded
+                              | mulW_noinline _ _ => apply mulW_correct_and_bounded
+                              | powW _ _ => apply powW_correct_and_bounded
+                              | sqrt_m1W => vm_compute; reflexivity
+                              | _ => assumption
+                              end
+                         end;
+             subst_evars; reflexivity
+      end.
     } Unfocus.
     lazymatch goal with
     | [ |- context G[dlet x := ?v in fe2213_32WToZ (@?f x)] ]
       => let G' := context G[fe2213_32WToZ (dlet x := v in f x)] in
          cut G'; cbv beta;
            [ cbv [Let_In]; exact (fun x => x) | apply f_equal ]
+    | _ => idtac
     end;
       reflexivity. }
   { cbv [Let_In];
-      break_if;
-      [ apply powW_correct_and_bounded; assumption
-      |  apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ];
-         apply powW_correct_and_bounded; assumption ]. }
+      try break_if;
+      repeat lazymatch goal with
+             | [ |- is_bounded (?WToZ (powW _ _)) = true ]
+               => apply powW_correct_and_bounded; assumption
+             | [ |- is_bounded (?WToZ (mulW _ _)) = true ]
+               => apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]
+             end. }
 Defined.
 
 Definition sqrtW (f : fe2213_32W) : fe2213_32W :=
diff --git a/src/SpecificGen/GF2519_32Bounded.v b/src/SpecificGen/GF2519_32Bounded.v
index 73e6ac193..9cb723690 100644
--- a/src/SpecificGen/GF2519_32Bounded.v
+++ b/src/SpecificGen/GF2519_32Bounded.v
@@ -294,7 +294,6 @@ Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe2519_32W_word64ize word64ize andb o
 
 Definition GF2519_32sqrt (x : GF2519_32.fe2519_32) : GF2519_32.fe2519_32.
 Proof.
-Print GF2519_32.sqrt.
   lazymatch (eval cbv delta [GF2519_32.sqrt] in GF2519_32.sqrt) with
   | (fun powf powf_squared f => dlet a := powf in _)
     => exact (dlet powx := powW (fe2519_32ZToW x) (chain GF2519_32.sqrt_ec) in
@@ -319,26 +318,26 @@ Proof.
         => apply powW_correct_and_bounded; assumption
       | [ |- _ = (dlet powx := _ in _) ]
         => apply Proper_Let_In_nd_changebody_eq; intros;
-        set_evars;
-        match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
-        | [ |- ?x = dlet y := fe2519_32WToZ ?z in ?f ]
-          => is_var z; change (x = match fe2519_32WToZ z with y => f end)
-        end;
-        change sqrt_m1 with (fe2519_32WToZ sqrt_m1W);
-        rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe2519_32WToZ)
-          by repeat match goal with
-                    | _ => progress subst
-                    | [ |- is_bounded (fe2519_32WToZ ?op) = true ]
-                      => lazymatch op with
-                         | mulW _ _ => apply mulW_correct_and_bounded
-                         | mulW_noinline _ _ => apply mulW_correct_and_bounded
-                         | powW _ _ => apply powW_correct_and_bounded
-                         | sqrt_m1W => vm_compute; reflexivity
-                         | _ => assumption
-                         end
-                    end;
-        subst_evars; reflexivity
-                       end.
+             set_evars;
+             match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
+             | [ |- ?x = dlet y := fe2519_32WToZ ?z in ?f ]
+               => is_var z; change (x = match fe2519_32WToZ z with y => f end)
+             end;
+             change sqrt_m1 with (fe2519_32WToZ sqrt_m1W);
+             rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe2519_32WToZ)
+               by repeat match goal with
+                         | _ => progress subst
+                         | [ |- is_bounded (fe2519_32WToZ ?op) = true ]
+                           => lazymatch op with
+                              | mulW _ _ => apply mulW_correct_and_bounded
+                              | mulW_noinline _ _ => apply mulW_correct_and_bounded
+                              | powW _ _ => apply powW_correct_and_bounded
+                              | sqrt_m1W => vm_compute; reflexivity
+                              | _ => assumption
+                              end
+                         end;
+             subst_evars; reflexivity
+      end.
     } Unfocus.
     lazymatch goal with
     | [ |- context G[dlet x := ?v in fe2519_32WToZ (@?f x)] ]
@@ -355,8 +354,7 @@ Proof.
                => apply powW_correct_and_bounded; assumption
              | [ |- is_bounded (?WToZ (mulW _ _)) = true ]
                => apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]
-             end.
-  }
+             end. }
 Defined.
 
 Definition sqrtW (f : fe2519_32W) : fe2519_32W :=
diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v
index 1898b9781..03a1bb125 100644
--- a/src/SpecificGen/GF25519_32Bounded.v
+++ b/src/SpecificGen/GF25519_32Bounded.v
@@ -294,7 +294,6 @@ Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519_32W_word64ize word64ize andb
 
 Definition GF25519_32sqrt (x : GF25519_32.fe25519_32) : GF25519_32.fe25519_32.
 Proof.
-Print GF25519_32.sqrt.
   lazymatch (eval cbv delta [GF25519_32.sqrt] in GF25519_32.sqrt) with
   | (fun powf powf_squared f => dlet a := powf in _)
     => exact (dlet powx := powW (fe25519_32ZToW x) (chain GF25519_32.sqrt_ec) in
@@ -314,39 +313,48 @@ Proof.
   split.
   { etransitivity.
     Focus 2. {
-      apply Proper_Let_In_nd_changebody_eq; intros;
-        set_evars;
-        match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
-        | [ |- ?x = dlet y := fe25519_32WToZ ?z in ?f ]
-          => is_var z; change (x = match fe25519_32WToZ z with y => f end)
-        end;
-        change sqrt_m1 with (fe25519_32WToZ sqrt_m1W);
-        rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519_32WToZ)
-          by repeat match goal with
-                    | _ => progress subst
-                    | [ |- is_bounded (fe25519_32WToZ ?op) = true ]
-                      => lazymatch op with
-                         | mulW _ _ => apply mulW_correct_and_bounded
-                         | mulW_noinline _ _ => apply mulW_correct_and_bounded
-                         | powW _ _ => apply powW_correct_and_bounded
-                         | sqrt_m1W => vm_compute; reflexivity
-                         | _ => assumption
-                         end
-                    end;
-        subst_evars; reflexivity.
+      lazymatch goal with
+      | [ |- _ = pow _ _ ]
+        => apply powW_correct_and_bounded; assumption
+      | [ |- _ = (dlet powx := _ in _) ]
+        => apply Proper_Let_In_nd_changebody_eq; intros;
+             set_evars;
+             match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
+             | [ |- ?x = dlet y := fe25519_32WToZ ?z in ?f ]
+               => is_var z; change (x = match fe25519_32WToZ z with y => f end)
+             end;
+             change sqrt_m1 with (fe25519_32WToZ sqrt_m1W);
+             rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519_32WToZ)
+               by repeat match goal with
+                         | _ => progress subst
+                         | [ |- is_bounded (fe25519_32WToZ ?op) = true ]
+                           => lazymatch op with
+                              | mulW _ _ => apply mulW_correct_and_bounded
+                              | mulW_noinline _ _ => apply mulW_correct_and_bounded
+                              | powW _ _ => apply powW_correct_and_bounded
+                              | sqrt_m1W => vm_compute; reflexivity
+                              | _ => assumption
+                              end
+                         end;
+             subst_evars; reflexivity
+      end.
     } Unfocus.
     lazymatch goal with
     | [ |- context G[dlet x := ?v in fe25519_32WToZ (@?f x)] ]
       => let G' := context G[fe25519_32WToZ (dlet x := v in f x)] in
          cut G'; cbv beta;
            [ cbv [Let_In]; exact (fun x => x) | apply f_equal ]
+    | _ => idtac
     end;
       reflexivity. }
   { cbv [Let_In];
-      break_if;
-      [ apply powW_correct_and_bounded; assumption
-      |  apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ];
-         apply powW_correct_and_bounded; assumption ]. }
+      try break_if;
+      repeat lazymatch goal with
+             | [ |- is_bounded (?WToZ (powW _ _)) = true ]
+               => apply powW_correct_and_bounded; assumption
+             | [ |- is_bounded (?WToZ (mulW _ _)) = true ]
+               => apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]
+             end. }
 Defined.
 
 Definition sqrtW (f : fe25519_32W) : fe25519_32W :=
diff --git a/src/SpecificGen/GF25519_64Bounded.v b/src/SpecificGen/GF25519_64Bounded.v
index 37ee078ce..8100182ed 100644
--- a/src/SpecificGen/GF25519_64Bounded.v
+++ b/src/SpecificGen/GF25519_64Bounded.v
@@ -294,7 +294,6 @@ Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519_64W_word128ize word128ize and
 
 Definition GF25519_64sqrt (x : GF25519_64.fe25519_64) : GF25519_64.fe25519_64.
 Proof.
-Print GF25519_64.sqrt.
   lazymatch (eval cbv delta [GF25519_64.sqrt] in GF25519_64.sqrt) with
   | (fun powf powf_squared f => dlet a := powf in _)
     => exact (dlet powx := powW (fe25519_64ZToW x) (chain GF25519_64.sqrt_ec) in
@@ -314,39 +313,48 @@ Proof.
   split.
   { etransitivity.
     Focus 2. {
-      apply Proper_Let_In_nd_changebody_eq; intros;
-        set_evars;
-        match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
-        | [ |- ?x = dlet y := fe25519_64WToZ ?z in ?f ]
-          => is_var z; change (x = match fe25519_64WToZ z with y => f end)
-        end;
-        change sqrt_m1 with (fe25519_64WToZ sqrt_m1W);
-        rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519_64WToZ)
-          by repeat match goal with
-                    | _ => progress subst
-                    | [ |- is_bounded (fe25519_64WToZ ?op) = true ]
-                      => lazymatch op with
-                         | mulW _ _ => apply mulW_correct_and_bounded
-                         | mulW_noinline _ _ => apply mulW_correct_and_bounded
-                         | powW _ _ => apply powW_correct_and_bounded
-                         | sqrt_m1W => vm_compute; reflexivity
-                         | _ => assumption
-                         end
-                    end;
-        subst_evars; reflexivity.
+      lazymatch goal with
+      | [ |- _ = pow _ _ ]
+        => apply powW_correct_and_bounded; assumption
+      | [ |- _ = (dlet powx := _ in _) ]
+        => apply Proper_Let_In_nd_changebody_eq; intros;
+             set_evars;
+             match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
+             | [ |- ?x = dlet y := fe25519_64WToZ ?z in ?f ]
+               => is_var z; change (x = match fe25519_64WToZ z with y => f end)
+             end;
+             change sqrt_m1 with (fe25519_64WToZ sqrt_m1W);
+             rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519_64WToZ)
+               by repeat match goal with
+                         | _ => progress subst
+                         | [ |- is_bounded (fe25519_64WToZ ?op) = true ]
+                           => lazymatch op with
+                              | mulW _ _ => apply mulW_correct_and_bounded
+                              | mulW_noinline _ _ => apply mulW_correct_and_bounded
+                              | powW _ _ => apply powW_correct_and_bounded
+                              | sqrt_m1W => vm_compute; reflexivity
+                              | _ => assumption
+                              end
+                         end;
+             subst_evars; reflexivity
+      end.
     } Unfocus.
     lazymatch goal with
     | [ |- context G[dlet x := ?v in fe25519_64WToZ (@?f x)] ]
       => let G' := context G[fe25519_64WToZ (dlet x := v in f x)] in
          cut G'; cbv beta;
            [ cbv [Let_In]; exact (fun x => x) | apply f_equal ]
+    | _ => idtac
     end;
       reflexivity. }
   { cbv [Let_In];
-      break_if;
-      [ apply powW_correct_and_bounded; assumption
-      |  apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ];
-         apply powW_correct_and_bounded; assumption ]. }
+      try break_if;
+      repeat lazymatch goal with
+             | [ |- is_bounded (?WToZ (powW _ _)) = true ]
+               => apply powW_correct_and_bounded; assumption
+             | [ |- is_bounded (?WToZ (mulW _ _)) = true ]
+               => apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]
+             end. }
 Defined.
 
 Definition sqrtW (f : fe25519_64W) : fe25519_64W :=
diff --git a/src/SpecificGen/GF41417_32Bounded.v b/src/SpecificGen/GF41417_32Bounded.v
index 3e1bd49f7..17e8f70e7 100644
--- a/src/SpecificGen/GF41417_32Bounded.v
+++ b/src/SpecificGen/GF41417_32Bounded.v
@@ -294,7 +294,6 @@ Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe41417_32W_word64ize word64ize andb
 
 Definition GF41417_32sqrt (x : GF41417_32.fe41417_32) : GF41417_32.fe41417_32.
 Proof.
-Print GF41417_32.sqrt.
   lazymatch (eval cbv delta [GF41417_32.sqrt] in GF41417_32.sqrt) with
   | (fun powf powf_squared f => dlet a := powf in _)
     => exact (dlet powx := powW (fe41417_32ZToW x) (chain GF41417_32.sqrt_ec) in
@@ -314,39 +313,48 @@ Proof.
   split.
   { etransitivity.
     Focus 2. {
-      apply Proper_Let_In_nd_changebody_eq; intros;
-        set_evars;
-        match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
-        | [ |- ?x = dlet y := fe41417_32WToZ ?z in ?f ]
-          => is_var z; change (x = match fe41417_32WToZ z with y => f end)
-        end;
-        change sqrt_m1 with (fe41417_32WToZ sqrt_m1W);
-        rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe41417_32WToZ)
-          by repeat match goal with
-                    | _ => progress subst
-                    | [ |- is_bounded (fe41417_32WToZ ?op) = true ]
-                      => lazymatch op with
-                         | mulW _ _ => apply mulW_correct_and_bounded
-                         | mulW_noinline _ _ => apply mulW_correct_and_bounded
-                         | powW _ _ => apply powW_correct_and_bounded
-                         | sqrt_m1W => vm_compute; reflexivity
-                         | _ => assumption
-                         end
-                    end;
-        subst_evars; reflexivity.
+      lazymatch goal with
+      | [ |- _ = pow _ _ ]
+        => apply powW_correct_and_bounded; assumption
+      | [ |- _ = (dlet powx := _ in _) ]
+        => apply Proper_Let_In_nd_changebody_eq; intros;
+             set_evars;
+             match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
+             | [ |- ?x = dlet y := fe41417_32WToZ ?z in ?f ]
+               => is_var z; change (x = match fe41417_32WToZ z with y => f end)
+             end;
+             change sqrt_m1 with (fe41417_32WToZ sqrt_m1W);
+             rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe41417_32WToZ)
+               by repeat match goal with
+                         | _ => progress subst
+                         | [ |- is_bounded (fe41417_32WToZ ?op) = true ]
+                           => lazymatch op with
+                              | mulW _ _ => apply mulW_correct_and_bounded
+                              | mulW_noinline _ _ => apply mulW_correct_and_bounded
+                              | powW _ _ => apply powW_correct_and_bounded
+                              | sqrt_m1W => vm_compute; reflexivity
+                              | _ => assumption
+                              end
+                         end;
+             subst_evars; reflexivity
+      end.
     } Unfocus.
     lazymatch goal with
     | [ |- context G[dlet x := ?v in fe41417_32WToZ (@?f x)] ]
       => let G' := context G[fe41417_32WToZ (dlet x := v in f x)] in
          cut G'; cbv beta;
            [ cbv [Let_In]; exact (fun x => x) | apply f_equal ]
+    | _ => idtac
     end;
       reflexivity. }
   { cbv [Let_In];
-      break_if;
-      [ apply powW_correct_and_bounded; assumption
-      |  apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ];
-         apply powW_correct_and_bounded; assumption ]. }
+      try break_if;
+      repeat lazymatch goal with
+             | [ |- is_bounded (?WToZ (powW _ _)) = true ]
+               => apply powW_correct_and_bounded; assumption
+             | [ |- is_bounded (?WToZ (mulW _ _)) = true ]
+               => apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]
+             end. }
 Defined.
 
 Definition sqrtW (f : fe41417_32W) : fe41417_32W :=
diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v
index 881fc40f4..5bd8b85c2 100644
--- a/src/SpecificGen/GF5211_32Bounded.v
+++ b/src/SpecificGen/GF5211_32Bounded.v
@@ -294,7 +294,6 @@ Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe5211_32W_word64ize word64ize andb o
 
 Definition GF5211_32sqrt (x : GF5211_32.fe5211_32) : GF5211_32.fe5211_32.
 Proof.
-Print GF5211_32.sqrt.
   lazymatch (eval cbv delta [GF5211_32.sqrt] in GF5211_32.sqrt) with
   | (fun powf powf_squared f => dlet a := powf in _)
     => exact (dlet powx := powW (fe5211_32ZToW x) (chain GF5211_32.sqrt_ec) in
@@ -314,39 +313,48 @@ Proof.
   split.
   { etransitivity.
     Focus 2. {
-      apply Proper_Let_In_nd_changebody_eq; intros;
-        set_evars;
-        match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
-        | [ |- ?x = dlet y := fe5211_32WToZ ?z in ?f ]
-          => is_var z; change (x = match fe5211_32WToZ z with y => f end)
-        end;
-        change sqrt_m1 with (fe5211_32WToZ sqrt_m1W);
-        rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe5211_32WToZ)
-          by repeat match goal with
-                    | _ => progress subst
-                    | [ |- is_bounded (fe5211_32WToZ ?op) = true ]
-                      => lazymatch op with
-                         | mulW _ _ => apply mulW_correct_and_bounded
-                         | mulW_noinline _ _ => apply mulW_correct_and_bounded
-                         | powW _ _ => apply powW_correct_and_bounded
-                         | sqrt_m1W => vm_compute; reflexivity
-                         | _ => assumption
-                         end
-                    end;
-        subst_evars; reflexivity.
+      lazymatch goal with
+      | [ |- _ = pow _ _ ]
+        => apply powW_correct_and_bounded; assumption
+      | [ |- _ = (dlet powx := _ in _) ]
+        => apply Proper_Let_In_nd_changebody_eq; intros;
+             set_evars;
+             match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
+             | [ |- ?x = dlet y := fe5211_32WToZ ?z in ?f ]
+               => is_var z; change (x = match fe5211_32WToZ z with y => f end)
+             end;
+             change sqrt_m1 with (fe5211_32WToZ sqrt_m1W);
+             rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe5211_32WToZ)
+               by repeat match goal with
+                         | _ => progress subst
+                         | [ |- is_bounded (fe5211_32WToZ ?op) = true ]
+                           => lazymatch op with
+                              | mulW _ _ => apply mulW_correct_and_bounded
+                              | mulW_noinline _ _ => apply mulW_correct_and_bounded
+                              | powW _ _ => apply powW_correct_and_bounded
+                              | sqrt_m1W => vm_compute; reflexivity
+                              | _ => assumption
+                              end
+                         end;
+             subst_evars; reflexivity
+      end.
     } Unfocus.
     lazymatch goal with
     | [ |- context G[dlet x := ?v in fe5211_32WToZ (@?f x)] ]
       => let G' := context G[fe5211_32WToZ (dlet x := v in f x)] in
          cut G'; cbv beta;
            [ cbv [Let_In]; exact (fun x => x) | apply f_equal ]
+    | _ => idtac
     end;
       reflexivity. }
   { cbv [Let_In];
-      break_if;
-      [ apply powW_correct_and_bounded; assumption
-      |  apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ];
-         apply powW_correct_and_bounded; assumption ]. }
+      try break_if;
+      repeat lazymatch goal with
+             | [ |- is_bounded (?WToZ (powW _ _)) = true ]
+               => apply powW_correct_and_bounded; assumption
+             | [ |- is_bounded (?WToZ (mulW _ _)) = true ]
+               => apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]
+             end. }
 Defined.
 
 Definition sqrtW (f : fe5211_32W) : fe5211_32W :=