Module mathcomp.test_suite.test_regular_conv
From mathcomp Require Import boot order algebra field.Section regular.
Import GRing.
Goal forall R : ringType, [the lalgType R of R^o] = R :> ringType.
Proof.
by move=> [? []]. Qed.
Goal forall R : comRingType, [the algType R of R^o] = R :> ringType.
Proof.
by move=> [? []]. Qed.
Goal forall R : comRingType, [the comAlgType R of R^o] = R :> ringType.
Proof.
by move=> [? []]. Qed.
Goal forall R : comUnitRingType, [the unitAlgType R of R^o] = R :> unitRingType.
Proof.
by move=> [? []]. Qed.
Goal forall R : comUnitRingType,
[the comUnitAlgType R of R^o] = R :> comUnitRingType.
Proof.
by move=> [? []]. Qed.
Goal forall R : comUnitRingType, [the falgType R of R^o] = R :> unitRingType.
Proof.
by move=> [? []]. Qed.
Goal forall K : fieldType, [the fieldExtType K of K^o] = K :> fieldType.
Proof.
by move=> [? []]. Qed.
End regular.