fact: Record SORaddon := mk_SOR_addon { SORrm : ring_morph 0 1 rplus rtimes rminus ropp req cO cI cplus ctimes cminus copp ceqb phi; SORpower : power_theory rI rtimes req pow_phi rpow; SORcneqb_morph : forall x y : C, x [=] y = false -> [x] ~= [y]; SORcleb_morph : forall x y : C, x [<=] y = true -> [x] <= [y] }.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl