Require Import Crypto.SpecificGen.GF25519_32Reflective.Reified.Mul.
Require Export Crypto.Reflection.Z.JavaNotations.

Print rmulW.