proposition: Lemma ednatmulE x n : x *+ n = (x *+ n)%E.
proof: Proof. case: x => [x| |]; case: n => [//|n]. - by rewrite -EFin_natmul -EFin_dnatmul. - by rewrite enatmul_pinfty ednatmul_pinfty. - by rewrite enatmul_ninfty ednatmul_ninfty. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed