proposition: Lemma N2int_mul : {morph N2int : x y / x * y >-> mul x y}.
proof: Proof. move=> x y; apply Uint63.to_Z_inj. by rewrite Uint63.mul_spec !Uint63.of_Z_spec Nat2Z.inj_mul Zmult_mod. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63