diff options
Diffstat (limited to 'src/Experiments/NewPipeline/Toplevel1.v')
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 3b8f81ac6..e896e495f 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -1828,10 +1828,9 @@ Module Import UnsaturatedSolinas. rewrite ?map_map in *. cbn [lower upper] in *. split. - { etransitivity; [ erewrite <- eval_zeros; [ | apply weight_0, wprops ] | apply H15 ]. + { etransitivity; [ erewrite <- eval_zeros | apply H15 ]. apply Z.eq_le_incl; f_equal. - repeat match goal with H : _ |- _ => revert H end; exact admit. - omega. } + repeat match goal with H : _ |- _ => revert H end; exact admit. } { eapply Z.le_lt_trans; [ apply H15 | ]. assert (Hlen : length (encode (weight (Qnum limbwidth) (QDen limbwidth)) n s c (s - 1)) = n) by distr_length. revert Hlen. |