(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp.ssreflect
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
From mathcomp.discrete
Require Import choice fintype finset.
From mathcomp.fingroup
Require Import fingroup morphism perm action.
Require Import ssralg.

(*****************************************************************************)
(* This file clones the entire ssralg hierachy for finite types; this allows *)
(* type inference to function properly on expressions that mix combinatorial *)
(* and algebraic operators (e.g., [set x + y | x in A, y in A]).             *)
(*   finZmodType, finRingType, finComRingType, finUnitRingType,              *)
(*   finComUnitRingType, finIdomType, finFieldType finLmodType,              *)
(*   finLalgType finAlgType finUnitAlgType                                   *)
(*      == the finite counterparts of zmodType, etc.                         *)
(* Note that a finFieldType is canonically decidable. All these structures   *)
(* can be derived using [xxxType of T] forms, e.g., if R has both canonical  *)
(* finType and ringType structures, then                                     *)
(*     Canonical R_finRingType := Eval hnf in [finRingType of R].            *)
(* declares the derived finRingType structure for R. As the implementation   *)
(* of the derivation is somewhat involved, the Eval hnf normalization is     *)
(* strongly recommended.                                                     *)
(*   This file also provides direct tie-ins with finite group theory:        *)
(*  [baseFinGroupType of R for +%R] == the (canonical) additive group        *)
(*      [finGroupType of R for +%R]    structures for R                      *)
(*                         {unit R} == the type of units of R, which has a   *)
(*                                     canonical group structure.            *)
(*                FinRing.unit R Ux == the element of {unit R} corresponding *)
(*                                     to x, where Ux : x \in GRing.unit.    *)
(*                           'U%act == the action by right multiplication of *)
(*                                     {unit R} on R, via FinRing.unit_act.  *)
(*                                     (This is also a group action.)        *)
(*****************************************************************************)

Local Open Scope ring_scope.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module FinRing.

Local Notation mixin_of T b := (Finite.mixin_of (EqType T b)).

Section Generic.

(* Implicits *)
Variables (type base_type : Type) (class_of base_of : Type -> Type).
Variable to_choice : forall T, base_of T -> Choice.class_of T.
Variable base_sort : base_type -> Type.

(* Explicits *)
Variable Pack : forall T, class_of T -> Type -> type.
Variable Class : forall T b, mixin_of T (to_choice b) -> class_of T.
Variable base_class : forall bT, base_of (base_sort bT).

Definition gen_pack T :=
  fun bT b & phant_id (base_class bT) b =>
  fun fT m & phant_id (Finite.class fT) (Finite.Class m) =>
  Pack (@Class T b m) T.

End Generic.

Implicit Arguments
  gen_pack [type base_type class_of base_of to_choice base_sort].
Local Notation fin_ c := (@Finite.Class _ c c).
Local Notation do_pack pack T := (pack T _ _ id _ _ id).
Import GRing.Theory.

Definition groupMixin V := FinGroup.Mixin (@addrA V) (@add0r V) (@addNr V).
Local Notation base_group T vT fT :=
  (@FinGroup.PackBase T (groupMixin vT) (Finite.class fT)).
Local Notation fin_group B V := (@FinGroup.Pack B (@addNr V)).

Module Zmodule.

Section ClassDef.

Record class_of M :=
  Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M base }.
Local Coercion base : class_of >-> GRing.Zmodule.class_of.
Local Coercion mixin : class_of >-> mixin_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Zmodule.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.

Definition join_finType := @Finite.Pack zmodType (fin_ xclass) xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Zmodule.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Canonical join_finType.
Notation finZmodType := type.
Notation "[ 'finZmodType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'finZmodType'  'of'  T ]") : form_scope.
Coercion baseFinGroupType : type >-> FinGroup.base_type.
Canonical baseFinGroupType.
Coercion finGroupType : type >-> FinGroup.type.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
Notation "[ 'baseFinGroupType' 'of' R 'for' +%R ]" :=
    (BaseFinGroupType R (groupMixin _))
  (at level 0, format "[ 'baseFinGroupType'  'of'  R  'for'  +%R ]")
    : form_scope.
Notation "[ 'finGroupType' 'of' R 'for' +%R ]" :=
    (@FinGroup.clone R _ (finGroupType _) id _ id)
  (at level 0, format "[ 'finGroupType'  'of'  R  'for'  +%R ]") : form_scope.
End Exports.

End Zmodule.
Import Zmodule.Exports.

Section AdditiveGroup.

Variable U : finZmodType.
Implicit Types x y : U.

Lemma zmod1gE : 1%g = 0 :> U.            Proof. by []. Qed.
Lemma zmodVgE x : x^-1%g = - x.          Proof. by []. Qed.
Lemma zmodMgE x y : (x * y)%g = x + y.   Proof. by []. Qed.
Lemma zmodXgE n x : (x ^+ n)%g = x *+ n. Proof. by []. Qed.
Lemma zmod_mulgC x y : commute x y.      Proof. exact: GRing.addrC. Qed.
Lemma zmod_abelian (A : {set U}) : abelian A.
Proof. by apply/centsP=> x _ y _; exact: zmod_mulgC. Qed.

End AdditiveGroup.

Module Ring.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.Ring.class_of R; mixin : mixin_of R base }.
Definition base2 R (c : class_of R) := Zmodule.Class (mixin c).
Local Coercion base : class_of >-> GRing.Ring.class_of.
Local Coercion base2 : class_of >-> Zmodule.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Ring.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) cT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass cT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition join_finType := @Finite.Pack ringType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack ringType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Import Exports.
Coercion base : class_of >-> GRing.Ring.class_of.
Coercion base2 : class_of >-> Zmodule.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Canonical join_finType.
Canonical join_finZmodType.
Notation finRingType := type.
Notation "[ 'finRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'finRingType'  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

Section Unit.

Variable R : finRingType.

Definition is_inv (x y : R) := (x * y == 1) && (y * x == 1).
Definition unit := [qualify a x : R | [exists y, is_inv x y]].
Definition inv x := odflt x (pick (is_inv x)).

Lemma mulVr : {in unit, left_inverse 1 inv *%R}.
Proof.
rewrite /inv => x Ux; case: pickP => [y | no_y]; last by case/pred0P: Ux.
by case/andP=> _; move/eqP.
Qed.

Lemma mulrV : {in unit, right_inverse 1 inv *%R}.
Proof.
rewrite /inv => x Ux; case: pickP => [y | no_y]; last by case/pred0P: Ux.
by case/andP; move/eqP.
Qed.

Lemma intro_unit x y : y * x = 1 /\ x * y = 1 -> x \is a unit.
Proof.
by case=> yx1 xy1; apply/existsP; exists y; rewrite /is_inv xy1 yx1 !eqxx.
Qed.

Lemma invr_out : {in [predC unit], inv =1 id}.
Proof.
rewrite /inv => x nUx; case: pickP => // y invxy.
by case/existsP: nUx; exists y.
Qed.

Definition UnitMixin := GRing.UnitRing.Mixin mulVr mulrV intro_unit invr_out.

End Unit.

End Ring.
Import Ring.Exports.

Module ComRing.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.ComRing.class_of R; mixin : mixin_of R base }.
Definition base2 R (c : class_of R) := Ring.Class (mixin c).
Local Coercion base : class_of >-> GRing.ComRing.class_of.
Local Coercion base2 : class_of >-> Ring.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.ComRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition finRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition join_finType := @Finite.Pack comRingType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack comRingType xclass xT.
Definition join_finRingType := @Ring.Pack comRingType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.ComRing.class_of.
Coercion base2 : class_of >-> Ring.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finRingType.
Notation finComRingType := FinRing.ComRing.type.
Notation "[ 'finComRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'finComRingType'  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End ComRing.
Import ComRing.Exports.

Module UnitRing.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.UnitRing.class_of R; mixin : mixin_of R base }.
Definition base2 R (c : class_of R) := Ring.Class (mixin c).
Local Coercion base : class_of >-> GRing.UnitRing.class_of.
Local Coercion base2 : class_of >-> Ring.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.UnitRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition finRingType := @Ring.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.

Definition join_finType := @Finite.Pack unitRingType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack unitRingType xclass xT.
Definition join_finRingType := @Ring.Pack unitRingType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.UnitRing.class_of.
Coercion base2 : class_of >-> Ring.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finRingType.
Notation finUnitRingType := FinRing.UnitRing.type.
Notation "[ 'finUnitRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'finUnitRingType'  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End UnitRing.
Import UnitRing.Exports.

Section UnitsGroup.

Variable R : finUnitRingType.

Inductive unit_of (phR : phant R) := Unit (x : R) of x \is a GRing.unit.
Bind Scope group_scope with unit_of.

Let phR := Phant R.
Local Notation uT := (unit_of phR).
Implicit Types u v : uT.
Definition uval u := let: Unit x _ := u in x.

Canonical unit_subType := [subType for uval].
Definition unit_eqMixin := Eval hnf in [eqMixin of uT by <:].
Canonical unit_eqType := Eval hnf in EqType uT unit_eqMixin.
Definition unit_choiceMixin := [choiceMixin of uT by <:].
Canonical unit_choiceType := Eval hnf in ChoiceType uT unit_choiceMixin.
Definition unit_countMixin := [countMixin of uT by <:].
Canonical unit_countType := Eval hnf in CountType uT unit_countMixin.
Canonical unit_subCountType := Eval hnf in [subCountType of uT].
Definition unit_finMixin := [finMixin of uT by <:].
Canonical unit_finType := Eval hnf in FinType uT unit_finMixin.
Canonical unit_subFinType := Eval hnf in [subFinType of uT].

Definition unit1 := Unit phR (@GRing.unitr1 _).
Lemma unit_inv_proof u : (val u)^-1 \is a GRing.unit.
Proof. by rewrite GRing.unitrV ?(valP u). Qed.
Definition unit_inv u := Unit phR (unit_inv_proof u).
Lemma unit_mul_proof u v : val u * val v \is a GRing.unit.
Proof. by rewrite (GRing.unitrMr _ (valP u)) ?(valP v). Qed.
Definition unit_mul u v := Unit phR (unit_mul_proof u v).
Lemma unit_muluA : associative unit_mul.
Proof. move=> u v w; apply: val_inj; exact: GRing.mulrA. Qed.
Lemma unit_mul1u : left_id unit1 unit_mul.
Proof. move=> u; apply: val_inj; exact: GRing.mul1r. Qed.
Lemma unit_mulVu : left_inverse unit1 unit_inv unit_mul.
Proof. move=> u; apply: val_inj; exact: GRing.mulVr (valP u). Qed.

Definition unit_GroupMixin := FinGroup.Mixin unit_muluA unit_mul1u unit_mulVu.
Canonical unit_baseFinGroupType :=
  Eval hnf in BaseFinGroupType uT unit_GroupMixin.
Canonical unit_finGroupType := Eval hnf in FinGroupType unit_mulVu.

Lemma val_unit1 : val (1%g : uT) = 1. Proof. by []. Qed.
Lemma val_unitM x y : val (x * y : uT)%g = val x * val y. Proof. by []. Qed.
Lemma val_unitV x : val (x^-1 : uT)%g = (val x)^-1. Proof. by []. Qed.
Lemma val_unitX n x : val (x ^+ n : uT)%g = val x ^+ n.
Proof. by case: n; last by elim=> //= n ->. Qed.

Definition unit_act x u := x * val u.
Lemma unit_actE x u : unit_act x u = x * val u. Proof. by []. Qed.

Canonical unit_action :=
  @TotalAction _ _ unit_act (@GRing.mulr1 _) (fun _ _ _ => GRing.mulrA _ _ _).
Lemma unit_is_groupAction : @is_groupAction _ R setT setT unit_action.
Proof.
move=> u _ /=; rewrite inE; apply/andP; split.
  by apply/subsetP=> x _; rewrite inE.
by apply/morphicP=> x y _ _; rewrite !actpermE /= [_ u]GRing.mulrDl.
Qed.
Canonical unit_groupAction := GroupAction unit_is_groupAction.

End UnitsGroup.

Module Import UnitsGroupExports.
Bind Scope group_scope with unit_of.
Canonical unit_subType.
Canonical unit_eqType.
Canonical unit_choiceType.
Canonical unit_countType.
Canonical unit_subCountType.
Canonical unit_finType.
Canonical unit_subFinType.
Canonical unit_baseFinGroupType.
Canonical unit_finGroupType.
Canonical unit_action.
Canonical unit_groupAction.
End UnitsGroupExports.

Notation unit R Ux := (Unit (Phant R) Ux).

Module ComUnitRing.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.ComUnitRing.class_of R; mixin : mixin_of R base }.
Definition base2 R (c : class_of R) := ComRing.Class (mixin c).
Definition base3 R (c : class_of R) := @UnitRing.Class R (base c) (mixin c).
Local Coercion base : class_of >-> GRing.ComUnitRing.class_of.
Local Coercion base2 : class_of >-> ComRing.class_of.
Local Coercion base3 : class_of >-> UnitRing.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.ComUnitRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition finRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition finComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.

Definition join_finType := @Finite.Pack comUnitRingType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack comUnitRingType xclass xT.
Definition join_finRingType := @Ring.Pack comUnitRingType xclass xT.
Definition join_finComRingType := @ComRing.Pack comUnitRingType xclass xT.
Definition join_finUnitRingType := @UnitRing.Pack comUnitRingType xclass xT.
Definition ujoin_finComRingType := @ComRing.Pack unitRingType xclass xT.
Definition cjoin_finUnitRingType := @UnitRing.Pack comRingType xclass xT.
Definition fcjoin_finUnitRingType := @UnitRing.Pack finComRingType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.ComUnitRing.class_of.
Coercion base2 : class_of >-> ComRing.class_of.
Coercion base3 : class_of >-> UnitRing.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion finComRingType : type >-> ComRing.type.
Canonical finComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finRingType.
Canonical join_finComRingType.
Canonical join_finUnitRingType.
Canonical ujoin_finComRingType.
Canonical cjoin_finUnitRingType.
Canonical fcjoin_finUnitRingType.
Notation finComUnitRingType := FinRing.ComUnitRing.type.
Notation "[ 'finComUnitRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'finComUnitRingType'  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End ComUnitRing.
Import ComUnitRing.Exports.

Module IntegralDomain.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.IntegralDomain.class_of R; mixin : mixin_of R base }.
Definition base2 R (c : class_of R) := ComUnitRing.Class (mixin c).
Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Local Coercion base2 : class_of >-> ComUnitRing.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.IntegralDomain.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition finRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition finComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.

Definition join_finType := @Finite.Pack idomainType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack idomainType xclass xT.
Definition join_finRingType := @Ring.Pack idomainType xclass xT.
Definition join_finUnitRingType := @UnitRing.Pack idomainType xclass xT.
Definition join_finComRingType := @ComRing.Pack idomainType xclass xT.
Definition join_finComUnitRingType := @ComUnitRing.Pack idomainType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Coercion base2 : class_of >-> ComUnitRing.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion finComRingType : type >-> ComRing.type.
Canonical finComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion finComUnitRingType : type >-> ComUnitRing.type.
Canonical finComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finRingType.
Canonical join_finComRingType.
Canonical join_finUnitRingType.
Canonical join_finComUnitRingType.
Notation finIdomainType := FinRing.IntegralDomain.type.
Notation "[ 'finIdomainType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'finIdomainType'  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End IntegralDomain.
Import IntegralDomain.Exports.

Module Field.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.Field.class_of R; mixin : mixin_of R base }.
Definition base2 R (c : class_of R) := IntegralDomain.Class (mixin c).
Local Coercion base : class_of >-> GRing.Field.class_of.
Local Coercion base2 : class_of >-> IntegralDomain.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Field.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition finRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition finComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition finIdomainType := @IntegralDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.

Definition join_finType := @Finite.Pack fieldType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack fieldType xclass xT.
Definition join_finRingType := @Ring.Pack fieldType xclass xT.
Definition join_finUnitRingType := @UnitRing.Pack fieldType xclass xT.
Definition join_finComRingType := @ComRing.Pack fieldType xclass xT.
Definition join_finComUnitRingType := @ComUnitRing.Pack fieldType xclass xT.
Definition join_finIdomainType := @IntegralDomain.Pack fieldType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Field.class_of.
Coercion base2 : class_of >-> IntegralDomain.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion finComRingType : type >-> ComRing.type.
Canonical finComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion finComUnitRingType : type >-> ComUnitRing.type.
Canonical finComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion finIdomainType : type >-> IntegralDomain.type.
Canonical finIdomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finRingType.
Canonical join_finComRingType.
Canonical join_finUnitRingType.
Canonical join_finComUnitRingType.
Canonical join_finIdomainType.
Notation finFieldType := FinRing.Field.type.
Notation "[ 'finFieldType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'finFieldType'  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End Field.
Import Field.Exports.

Section DecideField.

Variable F : Field.type.

Fixpoint sat e f :=
  match f with
  | GRing.Bool b => b
  | t1 == t2 => (GRing.eval e t1 == GRing.eval e t2)%bool
  | GRing.Unit t => GRing.eval e t \is a GRing.unit
  | f1 /\ f2 => sat e f1 && sat e f2
  | f1 \/ f2 => sat e f1 || sat e f2
  | f1 ==> f2 => (sat e f1 ==> sat e f2)%bool
  | ~ f1 => ~~ sat e f1
  | ('exists 'X_k, f1) => [exists x : F, sat (set_nth 0%R e k x) f1]
  | ('forall 'X_k, f1) => [forall x : F, sat (set_nth 0%R e k x) f1]
  end%T.

Lemma decidable : GRing.DecidableField.axiom sat.
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; exact: idP.
- by move=> t1 t2 e; exact: eqP.
- by move=> t e; exact: idP.
- by move=> f IH e /=; case: IH; constructor.
- by move=> i f IH e; apply: (iffP existsP) => [] [x fx]; exists x; exact/IH.
by move=> i f IH e; apply: (iffP forallP) => f_ x; exact/IH.
Qed.

Definition DecidableFieldMixin := DecFieldMixin decidable.

End DecideField.

Module DecField.

Section Joins.

Variable cT : Field.type.
Let xT := let: Field.Pack T _ _ := cT in T.
Let xclass : Field.class_of xT := Field.class cT.

Definition type := Eval hnf in DecFieldType cT (DecidableFieldMixin cT).
Definition finType := @Finite.Pack type (fin_ xclass) xT.
Definition finZmodType := @Zmodule.Pack type xclass xT.
Definition finRingType := @Ring.Pack type xclass xT.
Definition finUnitRingType := @UnitRing.Pack type xclass xT.
Definition finComRingType := @ComRing.Pack type xclass xT.
Definition finComUnitRingType := @ComUnitRing.Pack type xclass xT.
Definition finIdomainType := @IntegralDomain.Pack type xclass xT.
Definition baseFinGroupType := base_group type finZmodType finZmodType.
Definition finGroupType := fin_group baseFinGroupType cT.

End Joins.

Module Exports.
Coercion type : Field.type >-> GRing.DecidableField.type.
Canonical type.
Canonical finType.
Canonical finZmodType.
Canonical finRingType.
Canonical finUnitRingType.
Canonical finComRingType.
Canonical finComUnitRingType.
Canonical finIdomainType.
Canonical baseFinGroupType.
Canonical finGroupType.
End Exports.

End DecField.

Module Lmodule.

Section ClassDef.

Variable R : ringType.

Record class_of M :=
  Class { base : GRing.Lmodule.class_of R M ; mixin : mixin_of M base }.
Definition base2 R (c : class_of R) := Zmodule.Class (mixin c).
Local Coercion base : class_of >-> GRing.Lmodule.class_of.
Local Coercion base2 : class_of >-> Zmodule.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition pack := gen_pack (Pack phR) Class (@GRing.Lmodule.class R phR).
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
Definition join_finType := @Finite.Pack lmodType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack lmodType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Import Exports.
Coercion base : class_of >-> GRing.Lmodule.class_of.
Coercion base2 : class_of >-> Zmodule.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion lmodType : type >-> GRing.Lmodule.type.
Canonical lmodType.
Canonical join_finType.
Canonical join_finZmodType.
Notation finLmodType R := (FinRing.Lmodule.type (Phant R)).
Notation "[ 'finLmodType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T)
  (at level 0, format "[ 'finLmodType'  R  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End Lmodule.
Import Lmodule.Exports.

Module Lalgebra.

Section ClassDef.

Variable R : ringType.

Record class_of M :=
  Class { base : GRing.Lalgebra.class_of R M; mixin : mixin_of M base }.
Definition base2 M (c : class_of M) := Ring.Class (mixin c).
Definition base3 M (c : class_of M) := @Lmodule.Class _ _ (base c) (mixin c).
Local Coercion base : class_of >-> GRing.Lalgebra.class_of.
Local Coercion base2 : class_of >-> Ring.class_of.
Local Coercion base3 : class_of >-> Lmodule.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition pack := gen_pack (Pack phR) Class (@GRing.Lalgebra.class R phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition finRingType := @Ring.Pack cT xclass xT.
Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.

Definition join_finType := @Finite.Pack lalgType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack lalgType xclass xT.
Definition join_finLmodType := @Lmodule.Pack R phR lalgType xclass xT.
Definition join_finRingType := @Ring.Pack lalgType xclass xT.
Definition rjoin_finLmodType := @Lmodule.Pack R phR ringType xclass xT.
Definition ljoin_finRingType := @Ring.Pack lmodType xclass xT.
Definition fljoin_finRingType := @Ring.Pack finLmodType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Lalgebra.class_of.
Coercion base2 : class_of >-> Ring.class_of.
Coercion base3 : class_of >-> Lmodule.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion lmodType : type >-> GRing.Lmodule.type.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finLmodType.
Canonical join_finRingType.
Canonical rjoin_finLmodType.
Canonical ljoin_finRingType.
Canonical fljoin_finRingType.
Notation finLalgType R := (FinRing.Lalgebra.type (Phant R)).
Notation "[ 'finLalgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T)
  (at level 0, format "[ 'finLalgType'  R  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End Lalgebra.
Import Lalgebra.Exports.

Module Algebra.

Section ClassDef.

Variable R : ringType.

Record class_of M :=
  Class { base : GRing.Algebra.class_of R M; mixin : mixin_of M base }.
Definition base2 M (c : class_of M) := Lalgebra.Class (mixin c).
Local Coercion base : class_of >-> GRing.Algebra.class_of.
Local Coercion base2 : class_of >->Lalgebra.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition pack := gen_pack (Pack phR) Class (@GRing.Algebra.class R phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (fin_ xclass) xT.
Definition finType := @Finite.Pack cT (fin_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition finZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition finRingType := @Ring.Pack cT xclass xT.
Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT.
Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.

Definition join_finType := @Finite.Pack algType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack algType xclass xT.
Definition join_finRingType := @Ring.Pack algType xclass xT.
Definition join_finLmodType := @Lmodule.Pack R phR algType xclass xT.
Definition join_finLalgType := @Lalgebra.Pack R phR algType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Algebra.class_of.
Coercion base2 : class_of >-> Lalgebra.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion lmodType : type >-> GRing.Lmodule.type.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion finLalgType : type >-> Lalgebra.type.
Canonical finLalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finLmodType.
Canonical join_finRingType.
Canonical join_finLalgType.
Notation finAlgType R := (type (Phant R)).
Notation "[ 'finAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T)
  (at level 0, format "[ 'finAlgType'  R  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End Algebra.
Import Algebra.Exports.

Module UnitAlgebra.
 
Section ClassDef.

Variable R : unitRingType.
 
Record class_of M := 
  Class { base : GRing.UnitAlgebra.class_of R M ; mixin : mixin_of M base }. 
Definition base2 M (c : class_of M) := Algebra.Class (mixin c).
Definition base3 M (c : class_of M) := @UnitRing.Class _ (base c) (mixin c).

Local Coercion base : class_of >-> GRing.UnitAlgebra.class_of.
Local Coercion base2 : class_of >-> Algebra.class_of.
Local Coercion base3 : class_of >-> UnitRing.class_of.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition pack := gen_pack (Pack phR) Class (@GRing.UnitAlgebra.class R phR). 
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT. 
Definition choiceType := @Choice.Pack cT xclass xT. 
Definition countType := @Countable.Pack cT (fin_ xclass) xT. 
Definition finType := @Finite.Pack cT (fin_ xclass) xT. 
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. 
Definition finZmodType := @Zmodule.Pack cT xclass xT. 
Definition ringType := @GRing.Ring.Pack cT xclass xT. 
Definition finRingType := @Ring.Pack cT xclass xT. 
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition finUnitRingType := @UnitRing.Pack cT xclass xT. 
Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. 
Definition finLmodType := @Lmodule.Pack R phR cT xclass xT. 
Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT. 
Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT. 
Definition algType := @GRing.Algebra.Pack R phR cT xclass xT. 
Definition finAlgType := @Algebra.Pack R phR cT xclass xT. 
Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.

Definition join_finType := @Finite.Pack unitAlgType (fin_ xclass) xT.
Definition join_finZmodType := @Zmodule.Pack unitAlgType xclass xT.
Definition join_finRingType := @Ring.Pack unitAlgType xclass xT.
Definition join_finUnitRingType := @UnitRing.Pack unitAlgType xclass xT.
Definition join_finLmodType := @Lmodule.Pack R phR unitAlgType xclass xT.
Definition join_finLalgType := @Lalgebra.Pack R phR unitAlgType xclass xT.
Definition join_finAlgType := @Algebra.Pack R phR unitAlgType xclass xT.
Definition  ljoin_finUnitRingType := @UnitRing.Pack lmodType xclass xT.
Definition fljoin_finUnitRingType := @UnitRing.Pack finLmodType xclass xT.
Definition  njoin_finUnitRingType := @UnitRing.Pack lalgType xclass xT.
Definition fnjoin_finUnitRingType := @UnitRing.Pack finLalgType xclass xT.
Definition  ajoin_finUnitRingType := @UnitRing.Pack algType xclass xT.
Definition fajoin_finUnitRingType := @UnitRing.Pack finAlgType xclass xT.
Definition ujoin_finLmodType := @Lmodule.Pack R phR unitRingType xclass xT.
Definition ujoin_finLalgType := @Lalgebra.Pack R phR unitRingType xclass xT.
Definition ujoin_finAlgType := @Algebra.Pack R phR unitRingType xclass xT.

Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
Definition join_baseFinGroupType := base_group zmodType zmodType finType.
Definition join_finGroupType := fin_group join_baseFinGroupType zmodType.

End ClassDef. 

Module Exports.
Coercion base : class_of >-> GRing.UnitAlgebra.class_of.
Coercion base2 : class_of >-> Algebra.class_of.
Coercion base3 : class_of >-> UnitRing.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion lmodType : type >-> GRing.Lmodule.type.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion finLalgType : type >-> Lalgebra.type.
Canonical finLalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
Coercion finAlgType : type >-> Algebra.type.
Canonical finAlgType.
Coercion unitAlgType : type >-> GRing.UnitAlgebra.type.
Canonical unitAlgType.
Canonical join_finType.
Canonical join_finZmodType.
Canonical join_finLmodType.
Canonical join_finRingType.
Canonical join_finLalgType.
Canonical join_finAlgType.
Canonical ljoin_finUnitRingType.
Canonical fljoin_finUnitRingType.
Canonical njoin_finUnitRingType.
Canonical fnjoin_finUnitRingType.
Canonical ajoin_finUnitRingType.
Canonical fajoin_finUnitRingType.
Canonical ujoin_finLmodType.
Canonical ujoin_finLalgType.
Canonical ujoin_finAlgType.
Notation finUnitAlgType R := (type (Phant R)).
Notation "[ 'finUnitAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T) 
  (at level 0, format "[ 'finUnitAlgType'  R  'of'  T ]") : form_scope.
Canonical baseFinGroupType.
Canonical finGroupType.
Canonical join_baseFinGroupType.
Canonical join_finGroupType.
End Exports.

End UnitAlgebra.
Import UnitAlgebra.Exports.

Module Theory.

Definition zmod1gE := zmod1gE.
Definition zmodVgE := zmodVgE.
Definition zmodMgE := zmodMgE.
Definition zmodXgE := zmodXgE.
Definition zmod_mulgC := zmod_mulgC.
Definition zmod_abelian := zmod_abelian.
Definition val_unit1 := val_unit1.
Definition val_unitM := val_unitM.
Definition val_unitX := val_unitX.
Definition val_unitV := val_unitV.
Definition unit_actE := unit_actE.

End Theory.

End FinRing.

Import FinRing.
Export Zmodule.Exports Ring.Exports ComRing.Exports.
Export UnitRing.Exports UnitsGroupExports ComUnitRing.Exports.
Export IntegralDomain.Exports Field.Exports DecField.Exports.    
Export Lmodule.Exports Lalgebra.Exports Algebra.Exports UnitAlgebra.Exports.

Notation "{ 'unit' R }" := (unit_of (Phant R))
  (at level 0, format "{ 'unit'  R }") : type_scope.
Prenex Implicits FinRing.uval.
Notation "''U'" := (unit_action _) (at level 8) : action_scope.
Notation "''U'" := (unit_groupAction _) (at level 8) : groupAction_scope.