diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index b28ce15b9..8df4b7c64 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -324,8 +324,13 @@ pr " Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z. Proof. - do_size (destruct n; [exact ZnZ.spec_0|]). - destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0. + do_size (destruct n; + [match goal with + |- @eq Z (_ (zeron ?n)) _ => + apply (ZnZ.spec_0 (Specs:=dom_spec n)) + end|]). + destruct n; auto. simpl. rewrite make_op_S. fold word. + apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))). Qed. (** * Digits *) |