proposition: Lemma char0_intr_inj : injective (fun i => i%:~R : R).
proof: Proof. move=> i j /eqP; rewrite -subr_eq0 -rmorphB /= char0_intr_eq0 subr_eq0. by move/eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra all_field)