proposition: Lemma mule_natl x n : n%:R%:E * x = x *+ n.
proof: Proof. elim: n => [|n]; first by rewrite mul0e. move: x => [x| |] ih. - by rewrite -EFinM mulr_natl EFin_natmul. - by rewrite mulry gtr0_sg// mul1e enatmul_pinfty. - by rewrite mulrNy gtr0_sg// mul1e enatmul_ninfty. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed