blob: ce95280fb1e5264efb3edab740005a669e38dd22 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Require Import Cyclic63.
Goal False.
Proof.
assert (4294967296 *c 2147483648 = WW 2 0)%int63 as H.
vm_cast_no_check (@eq_refl (zn2z int) (WW 2 0)%int63).
generalize (f_equal (zn2z_to_Z wB to_Z) H).
now rewrite mulc_WW_spec.
Fail Qed.
Abort.
|
