proposition: Lemma char0_ratr_inj : injective ratrL.
proof: Proof. suff inj0 z : ratrL z = 0 -> z = 0. move=> x y /eqP; rewrite -subr_eq0 -char0_ratrB => /eqP /inj0 /eqP. by rewrite subr_eq0 => /eqP. rewrite /ratrL /ratr; move/eqP; rewrite mulf_eq0 invr_eq0 orbC. have /negPf-> /= : (denq z)%:~R != 0 :> L by rewrite char0_intr_eq0 // denq_eq0. by rewrite char0_intr_eq0 // numq_eq0 => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra all_field)