proposition: Lemma decidable : GRing.decidable_field_axiom sat.
proof: Proof. move=> e f; elim: f e; try by move=> f1 IH1 f2 IH2 e /=; case IH1; case IH2; constructor; tauto. - by move=> b e; apply: idP. - by move=> t1 t2 e; apply: eqP. - by move=> t e; apply: idP. - by move=> f IH e /=; case: IH; constructor. - by move=> i f IH e; apply: (iffP existsP) => [] [x fx]; exists x; apply/IH. by move=> i f IH e; apply: (iffP forallP) => f_ x; apply/IH. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)