proposition: Lemma char0_intr_eq0 (z : int) : ((z%:~R : R) == 0) = (z == 0).
proof: Proof. suff hPos (m : nat) : (m%:~R == 0 :> R) = (Posz m == 0). by case: z => [m | m] => //; rewrite NegzE rmorphN /= !oppr_eq0. by rewrite [m%:~R]/(m%:R); move/charf0P: (charR0)->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra all_field)