fact: Definition Scorrect (R : comSemiRingType) := let RE := Eq_ext +%R *%R id in let RN := SRmorph_Rmorph (Eqsth R) (RN R) in ring_correct (Eqsth R) RE (SRth_ARth (Eqsth R) (RS R)) RN (PN R) (triv_div_th (Eqsth R) RE (SRth_ARth (Eqsth R) (RS R)) RN).
imports: elpi(elpi) Coq(ZArith Ring Ring_polynom Field_theory) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)