Library mathcomp.algebra.ssralg

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
From mathcomp Require Import choice fintype finfun bigop prime binomial.

The algebraic part of the Algebraic Hierarchy, as described in ``Packaging mathematical structures'', TPHOLs09, by Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau
This file defines for each Structure (Zmodule, Ring, etc ...) its type, its packers and its canonical properties :

Zmodule (additive abelian groups):

zmodType == interface type for Zmodule structure. ZmodMixin addA addC add0x addNx == builds the mixin for a Zmodule from the algebraic properties of its operations. ZmodType V m == packs the mixin m to build a Zmodule of type zmodType. The carrier type V must have a choiceType canonical structure. [zmodType of V for S] == V-clone of the zmodType structure S: a copy of S where the sort carrier has been replaced by V, and which is therefore a zmodType structure on V. The sort carrier for S must be convertible to V. [zmodType of V] == clone of a canonical zmodType structure on V. Similar to the above, except S is inferred, but possibly with a syntactically different carrier. 0 == the zero (additive identity) of a Zmodule. x + y == the sum of x and y (in a Zmodule).
  • x == the opposite (additive inverse) of x.
x - y == the difference of x and y; this is only notation for x + (- y). x *+ n == n times x, with n in nat (non-negative), i.e., x + (x + .. (x + x)..) (n terms); x *+ 1 is thus convertible to x, and x *+ 2 to x + x. x *- n == notation for - (x *+ n), the opposite of x *+ n. \sum<range> e == iterated sum for a Zmodule (cf bigop.v). e`_i == nth 0 e i, when e : seq M and M has a zmodType structure. support f == 0.-support f, i.e., [pred x | f x != 0]. oppr_closed S <-> collective predicate S is closed under opposite. addr_closed S <-> collective predicate S is closed under finite sums (0 and x + y in S, for x, y in S). zmod_closed S <-> collective predicate S is closed under zmodType operations (0 and x - y in S, for x, y in S). This property coerces to oppr_pred and addr_pred. OpprPred oppS == packs oppS : oppr_closed S into an opprPred S interface structure associating this property to the canonical pred_key S, i.e. the k for which S has a Canonical keyed_pred k structure (see file ssrbool.v). AddrPred addS == packs addS : addr_closed S into an addrPred S interface structure associating this property to the canonical pred_key S (see above). ZmodPred oppS == packs oppS : oppr_closed S into an zmodPred S interface structure associating the zmod_closed property to the canonical pred_key S (see above), which must already be an addrPred. [zmodMixin of M by <: ] == zmodType mixin for a subType whose base type is a zmodType and whose predicate's canonical pred_key is a zmodPred. > Coq can be made to behave as if all predicates had canonical zmodPred keys by executing Import DefaultKeying GRing.DefaultPred. The required oppr_closed and addr_closed assumptions will be either abstracted, resolved or issued as separate proof obligations by the ssreflect plugin abstraction and Prop-irrelevance functions.

Ring (non-commutative rings):

ringType == interface type for a Ring structure. RingMixin mulA mul1x mulx1 mulDx mulxD == builds the mixin for a Ring from the algebraic properties of its multiplicative operators; the carrier type must have a zmodType structure. RingType R m == packs the ring mixin m into a ringType. R^c == the converse Ring for R: R^c is convertible to R but when R has a canonical ringType structure R^c has the converse one: if x y : R^c, then x * y = (y : R) * (x : R). [ringType of R for S] == R-clone of the ringType structure S. [ringType of R] == clone of a canonical ringType structure on R. 1 == the multiplicative identity element of a Ring. n%:R == the ring image of an n in nat; this is just notation for 1 *+ n, so 1%:R is convertible to 1 and 2%:R to 1 + 1. <number> == <number>%:R with <number> a sequence of digits x * y == the ring product of x and y. \prod<range> e == iterated product for a ring (cf bigop.v). x ^+ n == x to the nth power with n in nat (non-negative), i.e., x * (x * .. (x * x)..) (n factors); x ^+ 1 is thus convertible to x, and x ^+ 2 to x * x. GRing.sign R b := (-1) ^+ b in R : ringType, with b : bool. This is a parsing-only helper notation, to be used for defining more specific instances. GRing.comm x y <-> x and y commute, i.e., x * y = y * x. GRing.lreg x <-> x if left-regular, i.e., *%R x is injective. GRing.rreg x <-> x if right-regular, i.e., *%R x is injective. [char R] == the characteristic of R, defined as the set of prime numbers p such that p%:R = 0 in R. The set [char R] has at most one element, and is implemented as a pred_nat collective predicate (see prime.v); thus the statement p \in [char R] can be read as `R has characteristic p', while [char R] =i pred0 means `R has characteristic 0' when R is a field. Frobenius_aut chRp == the Frobenius automorphism mapping x in R to x ^+ p, where chRp : p \in [char R] is a proof that R has (non-zero) characteristic p. mulr_closed S <-> collective predicate S is closed under finite products (1 and x * y in S for x, y in S). smulr_closed S <-> collective predicate S is closed under products and opposite (-1 and x * y in S for x, y in S). semiring_closed S <-> collective predicate S is closed under semiring operations (0, 1, x + y and x * y in S). subring_closed S <-> collective predicate S is closed under ring operations (1, x - y and x * y in S). MulrPred mulS == packs mulS : mulr_closed S into a mulrPred S, SmulrPred mulS smulrPred S, semiringPred S, or subringPred S SemiringPred mulS interface structure, corresponding to the above SubRingPred mulS properties, respectively, provided S already has the supplementary zmodType closure properties. The properties above coerce to subproperties so, e.g., ringS : subring_closed S can be used for the proof obligations of all prerequisites. [ringMixin of R by <: ] == ringType mixin for a subType whose base type is a ringType and whose predicate's canonical key is a SubringPred. > As for zmodType predicates, Import DefaultKeying GRing.DefaultPred turns unresolved GRing.Pred unification constraints into proof obligations for basic closure assumptions.

ComRing (commutative Rings):

comRingType == interface type for commutative ring structure. ComRingType R mulC == packs mulC into a comRingType; the carrier type R must have a ringType canonical structure. ComRingMixin mulA mulC mul1x mulDx == builds the mixin for a Ring (i.e., a *non commutative* ring), using the commutativity to reduce the number of proof obligations. [comRingType of R for S] == R-clone of the comRingType structure S. [comRingType of R] == clone of a canonical comRingType structure on R. [comRingMixin of R by <: ] == comutativity mixin axiom for R when it is a subType of a commutative ring.

UnitRing (Rings whose units have computable inverses):

unitRingType == interface type for the UnitRing structure. UnitRingMixin mulVr mulrV unitP inv0id == builds the mixin for a UnitRing from the properties of the inverse operation and the boolean test for being a unit (invertible). The inverse of a non-unit x is constrained to be x itself (property inv0id). The carrier type must have a ringType canonical structure. UnitRingType R m == packs the unit ring mixin m into a unitRingType. WARNING: while it is possible to omit R for most of the XxxType functions, R MUST be explicitly given when UnitRingType is used with a mixin produced by ComUnitRingMixin, in a Canonical definition, otherwise the resulting structure will have the WRONG sort key and will NOT BE USED during type inference. [unitRingType of R for S] == R-clone of the unitRingType structure S. [unitRingType of R] == clones a canonical unitRingType structure on R. x \is a GRing.unit <=> x is a unit (i.e., has an inverse). x^-1 == the ring inverse of x, if x is a unit, else x. x / y == x divided by y (notation for x * y^-1). x ^- n := notation for (x ^+ n)^-1, the inverse of x ^+ n. invr_closed S <-> collective predicate S is closed under inverse. divr_closed S <-> collective predicate S is closed under division (1 and x / y in S). sdivr_closed S <-> collective predicate S is closed under division and opposite (-1 and x / y in S, for x, y in S). divring_closed S <-> collective predicate S is closed under unitRing operations (1, x - y and x / y in S). DivrPred invS == packs invS : mulr_closed S into a divrPred S, SdivrPred invS sdivrPred S or divringPred S interface structure, DivringPred invS corresponding to the above properties, resp., provided S already has the supplementary ringType closure properties. The properties above coerce to subproperties, as explained above. [unitRingMixin of R by <: ] == unitRingType mixin for a subType whose base type is a unitRingType and whose predicate's canonical key is a divringPred and whose ring structure is compatible with the base type's.

ComUnitRing (commutative rings with computable inverses):

comUnitRingType == interface type for ComUnitRing structure. ComUnitRingMixin mulVr unitP inv0id == builds the mixin for a UnitRing (a *non commutative* unit ring, using commutativity to simplify the proof obligations; the carrier type must have a comRingType structure. WARNING: ALWAYS give an explicit type argument to UnitRingType along with a mixin produced by ComUnitRingMixin (see above). [comUnitRingType of R] == a comUnitRingType structure for R created by merging canonical comRingType and unitRingType structures on R.

IntegralDomain (integral, commutative, ring with partial inverses):

idomainType == interface type for the IntegralDomain structure. IdomainType R mulf_eq0 == packs the integrality property into an idomainType integral domain structure; R must have a comUnitRingType canonical structure. [idomainType of R for S] == R-clone of the idomainType structure S. [idomainType of R] == clone of a canonical idomainType structure on R. [idomainMixin of R by <: ] == mixin axiom for a idomain subType.

Field (commutative fields):

fieldType == interface type for fields. GRing.Field.mixin_of R == the field property: x != 0 -> x \is a unit, for x : R; R must be or coerce to a unitRingType. GRing.Field.axiom inv == the field axiom: x != 0 -> inv x * x = 1 for all x. This is equivalent to the property above, but does not require a unitRingType as inv is an explicit argument. FieldUnitMixin mulVf inv0 == a *non commutative unit ring* mixin, using an inverse function that satisfies the field axiom and fixes 0 (arguments mulVf and inv0, resp.), and x != 0 as the Ring.unit predicate. The carrier type must be a canonical comRingType. FieldIdomainMixin m == an *idomain* mixin derived from a field mixin m. GRing.Field.IdomainType mulVf inv0 == an idomainType incorporating the two mixins above, where FieldIdomainMixin is applied to the trivial field mixin for FieldUnitMixin. FieldMixin mulVf inv0 == the (trivial) field mixin for Field.IdomainType. FieldType R m == packs the field mixin M into a fieldType. The carrier type R must be an idomainType. > Given proofs mulVf and inv0 as above, a non-Canonical instances of fieldType can be created with FieldType _ (FieldMixin mulVf inv0). For Canonical instances one should always specify the first (sort) argument of FieldType and other instance constructors, as well as pose Definitions for unit ring, field, and idomain mixins (in that order). [fieldType of F for S] == F-clone of the fieldType structure S. [fieldType of F] == clone of a canonical fieldType structure on F. [fieldMixin of R by <: ] == mixin axiom for a field subType.

DecidableField (fields with a decidable first order theory):

decFieldType == interface type for DecidableField structure. DecFieldMixin satP == builds the mixin for a DecidableField from the correctness of its satisfiability predicate. The carrier type must have a unitRingType structure. DecFieldType F m == packs the decidable field mixin m into a decFieldType; the carrier type F must have a fieldType structure. [decFieldType of F for S] == F-clone of the decFieldType structure S. [decFieldType of F] == clone of a canonical decFieldType structure on F GRing.term R == the type of formal expressions in a unit ring R with formal variables 'X_k, k : nat, and manifest constants x%:T, x : R. The notation of all the ring operations is redefined for terms, in scope %T. GRing.formula R == the type of first order formulas over R; the %T scope binds the logical connectives /\, \/, ~, ==>, ==, and != to formulae; GRing.True/False and GRing.Bool b denote constant formulae, and quantifiers are written 'forall/'exists 'X_k, f. GRing.Unit x tests for ring units GRing.If p_f t_f e_f emulates if-then-else GRing.Pick p_f t_f e_f emulates fintype.pick foldr GRing.Exists/Forall q_f xs can be used to write iterated quantifiers. GRing.eval e t == the value of term t with valuation e : seq R (e maps 'X_i to e`_i). GRing.same_env e1 e2 <-> environments e1 and e2 are extensionally equal. GRing.qf_form f == f is quantifier-free. GRing.holds e f == the intuitionistic CiC interpretation of the formula f holds with valuation e. GRing.qf_eval e f == the value (in bool) of a quantifier-free f. GRing.sat e f == valuation e satisfies f (only in a decField). GRing.sol n f == a sequence e of size n such that e satisfies f, if one exists, or [:: ] if there is no such e. QEdecFieldMixin wfP okP == a decidable field Mixin built from a quantifier eliminator p and proofs wfP : GRing.wf_QE_proj p and okP : GRing.valid_QE_proj p that p returns well-formed and valid formulae, i.e., p i (u, v) is a quantifier-free formula equivalent to 'exists 'X_i, u1 == 0 /\ ... /\ u_m == 0 /\ v1 != 0 ... /\ v_n != 0

ClosedField (algebraically closed fields):

closedFieldType == interface type for the ClosedField structure. ClosedFieldType F m == packs the closed field mixin m into a closedFieldType. The carrier F must have a decFieldType structure. [closedFieldType of F on S] == F-clone of a closedFieldType structure S. [closedFieldType of F] == clone of a canonicalclosedFieldType structure on F.

Lmodule (module with left multiplication by external scalars).

lmodType R == interface type for an Lmodule structure with scalars of type R; R must have a ringType structure. LmodMixin scalA scal1v scalxD scalDv == builds an Lmodule mixin from the algebraic properties of the scaling operation; the module carrier type must have a zmodType structure, and the scalar carrier must have a ringType structure. LmodType R V m == packs the mixin v to build an Lmodule of type lmodType R. The carrier type V must have a zmodType structure. [lmodType R of V for S] == V-clone of an lmodType R structure S. [lmodType R of V] == clone of a canonical lmodType R structure on V. a *: v == v scaled by a, when v is in an Lmodule V and a is in the scalar Ring of V. scaler_closed S <-> collective predicate S is closed under scaling. linear_closed S <-> collective predicate S is closed under linear combinations (a *: u + v in S when u, v in S). submod_closed S <-> collective predicate S is closed under lmodType operations (0 and a *: u + v in S). SubmodPred scaleS == packs scaleS : scaler_closed S in a submodPred S interface structure corresponding to the above property, provided S's key is a zmodPred; submod_closed coerces to all the prerequisites. [lmodMixin of V by <: ] == mixin for a subType of an lmodType, whose predicate's key is a submodPred.

Lalgebra (left algebra, ring with scaling that associates on the left):

lalgType R == interface type for Lalgebra structures with scalars in R; R must have ringType structure. LalgType R V scalAl == packs scalAl : k (x y) = (k x) y into an Lalgebra of type lalgType R. The carrier type V must have both lmodType R and ringType canonical structures. R^o == the regular algebra of R: R^o is convertible to R, but when R has a ringType structure then R^o extends it to an lalgType structure by letting R act on itself: if x : R and y : R^o then x *: y = x * (y : R). k%:A == the image of the scalar k in an L-algebra; this is simply notation for k *: 1. [lalgType R of V for S] == V-clone the lalgType R structure S. [lalgType R of V] == clone of a canonical lalgType R structure on V. subalg_closed S <-> collective predicate S is closed under lalgType operations (1, a *: u + v and u * v in S). SubalgPred scaleS == packs scaleS : scaler_closed S in a subalgPred S interface structure corresponding to the above property, provided S's key is a subringPred; subalg_closed coerces to all the prerequisites. [lalgMixin of V by <: ] == mixin axiom for a subType of an lalgType.

Algebra (ring with scaling that associates both left and right):

algType R == type for Algebra structure with scalars in R. R should be a commutative ring. AlgType R A scalAr == packs scalAr : k (x y) = x (k y) into an Algebra Structure of type algType R. The carrier type A must have an lalgType R structure. CommAlgType R A == creates an Algebra structure for an A that has both lalgType R and comRingType structures. [algType R of V for S] == V-clone of an algType R structure on S. [algType R of V] == clone of a canonical algType R structure on V. [algMixin of V by <: ] == mixin axiom for a subType of an algType.

UnitAlgebra (algebra with computable inverses):

unitAlgType R == interface type for UnitAlgebra structure with scalars in R; R should have a unitRingType structure. [unitAlgType R of V] == a unitAlgType R structure for V created by merging canonical algType and unitRingType on V. divalg_closed S <-> collective predicate S is closed under all unitAlgType operations (1, a *: u + v and u / v are in S fo u, v in S). DivalgPred scaleS == packs scaleS : scaler_closed S in a divalgPred S interface structure corresponding to the above property, provided S's key is a divringPred; divalg_closed coerces to all the prerequisites.

ComAlgebra (commutative algebra):

comAlgType R == interface type for ComAlgebra structure with scalars in R; R should have a comRingType structure. [comAlgType R of V] == a comAlgType R structure for V created by merging canonical algType and comRingType on V.

ComUnitAlgebra (commutative algebra with computable inverses):

comUnitAlgType R == interface type for ComUnitAlgebra structure with scalars in R; R should have a comUnitRingType structure. [comUnitAlgType R of V] == a comUnitAlgType R structure for V created by merging canonical comAlgType and unitRingType on V.
In addition to this structure hierarchy, we also develop a separate, parallel hierarchy for morphisms linking these structures:

Additive (additive functions):

additive f <-> f of type U -> V is additive, i.e., f maps the Zmodule structure of U to that of V, 0 to 0,
  • to - and + to + (equivalently, binary - to -).
:= {morph f : u v / u - v}. {additive U -> V} == the interface type for a Structure (keyed on a function f : U -> V) that encapsulates the additive property; both U and V must have zmodType canonical structures. Additive add_f == packs add_f : additive f into an additive function structure of type {additive U -> V}. [additive of f as g] == an f-clone of the additive structure on the function g -- f and g must be convertible. [additive of f] == a clone of an existing additive structure on f.

RMorphism (ring morphisms):

multiplicative f <-> f of type R -> S is multiplicative, i.e., f maps 1 and * in R to 1 and * in S, respectively, R ans S must have canonical ringType structures. rmorphism f <-> f is a ring morphism, i.e., f is both additive and multiplicative. {rmorphism R -> S} == the interface type for ring morphisms, i.e., a Structure that encapsulates the rmorphism property for functions f : R -> S; both R and S must have ringType structures. RMorphism morph_f == packs morph_f : rmorphism f into a Ring morphism structure of type {rmorphism R -> S}. AddRMorphism mul_f == packs mul_f : multiplicative f into an rmorphism structure of type {rmorphism R -> S}; f must already have an {additive R -> S} structure. [rmorphism of f as g] == an f-clone of the rmorphism structure of g. [rmorphism of f] == a clone of an existing additive structure on f.
  • > If R and S are UnitRings the f also maps units to units and inverses of units to inverses; if R is a field then f is a field isomorphism between R and its image.
  • > As rmorphism coerces to both additive and multiplicative, all structures for f can be built from a single proof of rmorphism f.
  • > Additive properties (raddf_suffix, see below) are duplicated and specialised for RMorphism (as rmorph_suffix). This allows more precise rewriting and cleaner chaining: although raddf lemmas will recognize RMorphism functions, the converse will not hold (we cannot add reverse inheritance rules because of incomplete backtracking in the Canonical Projection unification), so one would have to insert a /= every time one switched from additive to multiplicative rules.
  • > The property duplication also means that it is not strictly necessary to declare all Additive instances.

Linear (linear functions):

scalable f <-> f of type U -> V is scalable, i.e., f morphs scaling on U to scaling on V, a *: _ to a *: _. U and V must both have lmodType R structures, for the same ringType R. scalable_for s f <-> f is scalable for scaling operator s, i.e., f morphs a *: _ to s a _; the range of f only need to be a zmodType. The scaling operator s should be one of *:%R (see scalable, above), *%R or a combination nu \; *%R or nu \; *:%R with nu : {rmorphism _}; otherwise some of the theory (e.g., the linearZ rule) will not apply. linear f <-> f of type U -> V is linear, i.e., f morphs linear combinations a *: u + v in U to similar linear combinations in V; U and V must both have lmodType R structures, for the same ringType R. := forall a, {morph f: u v / a *: u + v}. scalar f <-> f of type U -> R is a scalar function, i.e., f (a *: u + v) = a * f u + f v. linear_for s f <-> f is linear for the scaling operator s, i.e., f (a *: u + v) = s a (f u) + f v. The range of f only needs to be a zmodType, but s MUST be of the form described in in scalable_for paragraph for this predicate to type check. lmorphism f <-> f is both additive and scalable. This is in fact equivalent to linear f, although somewhat less convenient to prove. lmorphism_for s f <-> f is both additive and scalable for s. {linear U -> V} == the interface type for linear functions, i.e., a Structure that encapsulates the linear property for functions f : U -> V; both U and V must have lmodType R structures, for the same R. {scalar U} == the interface type for scalar functions, of type U -> R where U has an lmodType R structure. {linear U -> V | s} == the interface type for functions linear for s. Linear lin_f == packs lin_f : lmorphism_for s f into a linear function structure of type {linear U -> V | s}. As linear_for s f coerces to lmorphism_for s f, Linear can be used with lin_f : linear_for s f (indeed, that is the recommended usage). Note that as linear f, scalar f, {linear U -> V} and {scalar U} are simply notation for corresponding generic "_for" forms, Linear can be used for any of these special cases, transparently. AddLinear scal_f == packs scal_f : scalable_for s f into a {linear U -> V | s} structure; f must already have an additive structure; as with Linear, AddLinear can be used with lin_f : linear f, etc [linear of f as g] == an f-clone of the linear structure of g. [linear of f] == a clone of an existing linear structure on f. (a *: u)%Rlin == transient forms that simplify to a *: u, a * u, (a * u)%Rlin nu a *: u, and nu a * u, respectively, and are (a *:^nu u)%Rlin created by rewriting with the linearZ lemma. The (a *^nu u)%Rlin forms allows the RHS of linearZ to be matched reliably, using the GRing.Scale.law structure.
  • > Similarly to Ring morphisms, additive properties are specialized for linear functions.
  • > Although {scalar U} is convertible to {linear U -> R^o}, it does not actually use R^o, so that rewriting preserves the canonical structure of the range of scalar functions.
  • > The generic linearZ lemma uses a set of bespoke interface structures to ensure that both left-to-right and right-to-left rewriting work even in the presence of scaling functions that simplify non-trivially (e.g., idfun \; *%R). Because most of the canonical instances and projections are coercions the machinery will be mostly invisible (with only the {linear ...} structure and %Rlin notations showing), but users should beware that in (a *: f u)%Rlin, a actually occurs in the f u subterm.
  • > The simpler linear_LR, or more specialized linearZZ and scalarZ rules should be used instead of linearZ if there are complexity issues, as well as for explicit forward and backward application, as the main parameter of linearZ is a proper sub-interface of {linear fUV | s}.

LRMorphism (linear ring morphisms, i.e., algebra morphisms):

lrmorphism f <-> f of type A -> B is a linear Ring (Algebra) morphism: f is both additive, multiplicative and scalable. A and B must both have lalgType R canonical structures, for the same ringType R. lrmorphism_for s f <-> f a linear Ring morphism for the scaling operator s: f is additive, multiplicative and scalable for s. A must be an lalgType R, but B only needs to have a ringType structure. {lrmorphism A -> B} == the interface type for linear morphisms, i.e., a Structure that encapsulates the lrmorphism property for functions f : A -> B; both A and B must have lalgType R structures, for the same R. {lrmorphism A -> B | s} == the interface type for morphisms linear for s. LRmorphism lrmorph_f == packs lrmorph_f : lrmorphism_for s f into a linear morphism structure of type {lrmorphism A -> B | s}. Like Linear, LRmorphism can be used transparently for lrmorphism f. AddLRmorphism scal_f == packs scal_f : scalable_for s f into a linear morphism structure of type {lrmorphism A -> B | s}; f must already have an {rmorphism A -> B} structure, and AddLRmorphism can be applied to a linear_for s f, linear f, scalar f, etc argument, like AddLinear. [lrmorphism of f] == creates an lrmorphism structure from existing rmorphism and linear structures on f; this is the preferred way of creating lrmorphism structures.
  • > Linear and rmorphism properties do not need to be specialized for as we supply inheritance join instances in both directions.
Finally we supply some helper notation for morphisms: x^f == the image of x under some morphism. This notation is only reserved (not defined) here; it is bound locally in sections where some morphism is used heavily (e.g., the container morphism in the parametricity sections of poly and matrix, or the Frobenius section here). \0 == the constant null function, which has a canonical linear structure, and simplifies on application (see ssrfun.v). f \+ g == the additive composition of f and g, i.e., the function x |-> f x + g x; f \+ g is canonically linear when f and g are, and simplifies on application (see ssrfun.v). f \- g == the function x |-> f x - g x, canonically linear when f and g are, and simplifies on application. \- g == the function x |-> - f x, canonically linear when f is, and simplifies on application. k \*: f == the function x |-> k *: f x, which is canonically linear when f is and simplifies on application (this is a shorter alternative to *:%R k \o f). GRing.in_alg A == the ring morphism that injects R into A, where A has an lalgType R structure; GRing.in_alg A k simplifies to k%:A. a \*o f == the function x |-> a * f x, canonically linear linear when f is and its codomain is an algType and which simplifies on application. a \o* f == the function x |-> f x * a, canonically linear linear when f is and its codomain is an lalgType and which simplifies on application. f \* g == the function x |-> f x * g x; f \* g simplifies on application. The Lemmas about these structures are contained in both the GRing module and in the submodule GRing.Theory, which can be imported when unqualified access to the theory is needed (GRing.Theory also allows the unqualified use of additive, linear, Linear, etc). The main GRing module should NOT be imported. Notations are defined in scope ring_scope (delimiter %R), except term and formula notations, which are in term_scope (delimiter %T). This library also extends the conventional suffixes described in library ssrbool.v with the following: 0 -- ring 0, as in addr0 : x + 0 = x. 1 -- ring 1, as in mulr1 : x * 1 = x. D -- ring addition, as in linearD : f (u + v) = f u + f v. B -- ring subtraction, as in opprB : - (x - y) = y - x. M -- ring multiplication, as in invfM : (x * y)^-1 = x^-1 * y^-1. Mn -- ring by nat multiplication, as in raddfMn : f (x *+ n) = f x *+ n. N -- ring opposite, as in mulNr : (- x) * y = - (x * y). V -- ring inverse, as in mulVr : x^-1 * x = 1. X -- ring exponentiation, as in rmorphX : f (x ^+ n) = f x ^+ n. Z -- (left) module scaling, as in linearZ : f (a *: v) = s *: f v. The operator suffixes D, B, M and X are also used for the corresponding operations on nat, as in natrX : (m ^ n)%:R = m%:R ^+ n. For the binary power operator, a trailing "n" suffix is used to indicate the operator suffix applies to the left-hand ring argument, as in expr1n : 1 ^+ n = 1 vs. expr1 : x ^+ 1 = x.

Set Implicit Arguments.

Declare Scope ring_scope.
Declare Scope term_scope.
Declare Scope linear_ring_scope.

Reserved Notation "+%R" (at level 0).
Reserved Notation "-%R" (at level 0).
Reserved Notation "*%R" (at level 0, format " *%R").
Reserved Notation "*:%R" (at level 0, format " *:%R").
Reserved Notation "n %:R" (at level 2, left associativity, format "n %:R").
Reserved Notation "k %:A" (at level 2, left associativity, format "k %:A").
Reserved Notation "[ 'char' F ]" (at level 0, format "[ 'char' F ]").

Reserved Notation "x %:T" (at level 2, left associativity, format "x %:T").
Reserved Notation "''X_' i" (at level 8, i at level 2, format "''X_' i").
Patch for recurring Coq parser bug: Coq seg faults when a level 200 notation is used as a pattern.
Reserved Notation "''exists' ''X_' i , f"
  (at level 199, i at level 2, right associativity,
   format "'[hv' ''exists' ''X_' i , '/ ' f ']'").
Reserved Notation "''forall' ''X_' i , f"
  (at level 199, i at level 2, right associativity,
   format "'[hv' ''forall' ''X_' i , '/ ' f ']'").

Reserved Notation "x ^f" (at level 2, left associativity, format "x ^f").

Reserved Notation "\0" (at level 0).
Reserved Notation "f \+ g" (at level 50, left associativity).
Reserved Notation "f \- g" (at level 50, left associativity).
Reserved Notation "\- f" (at level 35, f at level 35).
Reserved Notation "a \*o f" (at level 40).
Reserved Notation "a \o* f" (at level 40).
Reserved Notation "a \*: f" (at level 40).
Reserved Notation "f \* g" (at level 40, left associativity).

Delimit Scope ring_scope with R.
Delimit Scope term_scope with T.
Local Open Scope ring_scope.

Module Import GRing.

Import Monoid.Theory.

Module Zmodule.

Record mixin_of (V : Type) : Type := Mixin {
  zero : V;
  opp : V V;
  add : V V V;
  _ : associative add;
  _ : commutative add;
  _ : left_id zero add;
  _ : left_inverse zero opp add
}.

Section ClassDef.

Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.

Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack m :=
  fun bT b & phant_id (Choice.class bT) bPack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Choice.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.
Notation zmodType := type.
Notation ZmodType T m := (@pack T m _ _ id).
Notation ZmodMixin := Mixin.
Notation "[ 'zmodType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'zmodType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'zmodType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'zmodType' 'of' T ]") : form_scope.
End Exports.

End Zmodule.
Import Zmodule.Exports.

Definition zero V := Zmodule.zero (Zmodule.class V).
Definition opp V := Zmodule.opp (Zmodule.class V).
Definition add V := Zmodule.add (Zmodule.class V).


Definition natmul V x n := nosimpl iterop _ n +%R x (zero V).




Section ZmoduleTheory.

Variable V : zmodType.
Implicit Types x y : V.

Lemma addrA : @associative V +%R.
Lemma addrC : @commutative V V +%R.
Lemma add0r : @left_id V V 0 +%R.
Lemma addNr : @left_inverse V V V 0 -%R +%R.

Lemma addr0 : @right_id V V 0 +%R.
Lemma addrN : @right_inverse V V V 0 -%R +%R.
Definition subrr := addrN.

Canonical add_monoid := Monoid.Law addrA add0r addr0.
Canonical add_comoid := Monoid.ComLaw addrC.

Lemma addrCA : @left_commutative V V +%R.
Lemma addrAC : @right_commutative V V +%R.
Lemma addrACA : @interchange V +%R +%R.

Lemma addKr : @left_loop V V -%R +%R.
Lemma addNKr : @rev_left_loop V V -%R +%R.
Lemma addrK : @right_loop V V -%R +%R.
Lemma addrNK : @rev_right_loop V V -%R +%R.
Definition subrK := addrNK.
Lemma subKr x : involutive (fun yx - y).
Lemma addrI : @right_injective V V V +%R.
Lemma addIr : @left_injective V V V +%R.
Lemma subrI : right_injective (fun x yx - y).
Lemma subIr : left_injective (fun x yx - y).
Lemma opprK : @involutive V -%R.
Lemma oppr_inj : @injective V V -%R.
Lemma oppr0 : -0 = 0 :> V.
Lemma oppr_eq0 x : (- x == 0) = (x == 0).

Lemma subr0 x : x - 0 = x.
Lemma sub0r x : 0 - x = - x.

Lemma opprB x y : - (x - y) = y - x.

Lemma opprD : {morph -%R: x y / x + y : V}.

Lemma addrKA z x y : (x + z) - (z + y) = x - y.

Lemma subrKA z x y : (x - z) + (z + y) = x + y.

Lemma addr0_eq x y : x + y = 0 - x = y.

Lemma subr0_eq x y : x - y = 0 x = y.

Lemma subr_eq x y z : (x - z == y) = (x == y + z).

Lemma subr_eq0 x y : (x - y == 0) = (x == y).

Lemma addr_eq0 x y : (x + y == 0) = (x == - y).

Lemma eqr_opp x y : (- x == - y) = (x == y).

Lemma eqr_oppLR x y : (- x == y) = (x == - y).

Lemma mulr0n x : x *+ 0 = 0.
Lemma mulr1n x : x *+ 1 = x.
Lemma mulr2n x : x *+ 2 = x + x.

Lemma mulrS x n : x *+ n.+1 = x + x *+ n.

Lemma mulrSr x n : x *+ n.+1 = x *+ n + x.

Lemma mulrb x (b : bool) : x *+ b = (if b then x else 0).

Lemma mul0rn n : 0 *+ n = 0 :> V.

Lemma mulNrn x n : (- x) *+ n = x *- n.

Lemma mulrnDl n : {morph (fun xx *+ n) : x y / x + y}.

Lemma mulrnDr x m n : x *+ (m + n) = x *+ m + x *+ n.

Lemma mulrnBl n : {morph (fun xx *+ n) : x y / x - y}.

Lemma mulrnBr x m n : n m x *+ (m - n) = x *+ m - x *+ n.

Lemma mulrnA x m n : x *+ (m × n) = x *+ m *+ n.

Lemma mulrnAC x m n : x *+ m *+ n = x *+ n *+ m.

Lemma iter_addr n x y : iter n (+%R x) y = x *+ n + y.

Lemma iter_addr_0 n x : iter n (+%R x) 0 = x *+ n.

Lemma sumrN I r P (F : I V) :
  (\sum_(i <- r | P i) - F i = - (\sum_(i <- r | P i) F i)).

Lemma sumrB I r (P : pred I) (F1 F2 : I V) :
  \sum_(i <- r | P i) (F1 i - F2 i)
     = \sum_(i <- r | P i) F1 i - \sum_(i <- r | P i) F2 i.

Lemma sumrMnl I r P (F : I V) n :
  \sum_(i <- r | P i) F i *+ n = (\sum_(i <- r | P i) F i) *+ n.

Lemma sumrMnr x I r P (F : I nat) :
  \sum_(i <- r | P i) x *+ F i = x *+ (\sum_(i <- r | P i) F i).

Lemma sumr_const (I : finType) (A : pred I) x : \sum_(i in A) x = x *+ #|A|.

Lemma sumr_const_nat m n x : \sum_(n i < m) x = x *+ (m - n).

Lemma telescope_sumr n m (f : nat V) : n m
  \sum_(n k < m) (f k.+1 - f k) = f m - f n.

Lemma telescope_sumr_eq n m (f u : nat V) : n m
    ( k, (n k < m)%N u k = f k.+1 - f k)
  \sum_(n k < m) u k = f m - f n.

Section ClosedPredicates.

Variable S : {pred V}.

Definition addr_closed := 0 \in S {in S &, u v, u + v \in S}.
Definition oppr_closed := {in S, u, - u \in S}.
Definition subr_2closed := {in S &, u v, u - v \in S}.
Definition zmod_closed := 0 \in S subr_2closed.

Lemma zmod_closedN : zmod_closed oppr_closed.

Lemma zmod_closedD : zmod_closed addr_closed.

End ClosedPredicates.

End ZmoduleTheory.

Arguments addrI {V} y [x1 x2].
Arguments addIr {V} x [x1 x2].
Arguments opprK {V}.
Arguments oppr_inj {V} [x1 x2].
Arguments telescope_sumr_eq {V n m} f u.

Module Ring.

Record mixin_of (R : zmodType) : Type := Mixin {
  one : R;
  mul : R R R;
  _ : associative mul;
  _ : left_id one mul;
  _ : right_id one mul;
  _ : left_distributive mul +%R;
  _ : right_distributive mul +%R;
  _ : one != 0
}.

Definition EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 :=
  let _ := @Mixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 in
  @Mixin (Zmodule.Pack (Zmodule.class R)) _ _
     mulA mul1x mulx1 mul_addl mul_addr nz1.

Section ClassDef.

Record class_of (R : Type) : Type := Class {
  base : Zmodule.class_of R;
  mixin : mixin_of (Zmodule.Pack base)
}.

Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0)) :=
  fun bT b & phant_id (Zmodule.class bT) b
  fun m & phant_id m0 mPack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> 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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Notation ringType := type.
Notation RingType T m := (@pack T _ m _ _ id _ id).
Notation RingMixin := Mixin.
Notation "[ 'ringType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'ringType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'ringType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'ringType' 'of' T ]") : form_scope.
End Exports.

End Ring.
Import Ring.Exports.

Definition one (R : ringType) : R := Ring.one (Ring.class R).
Definition mul (R : ringType) : R R R := Ring.mul (Ring.class R).
Definition exp R x n := nosimpl iterop _ n (@mul R) x (one R).
Notation sign R b := (exp (- one R) (nat_of_bool b)) (only parsing).
Definition comm R x y := @mul R x y = mul y x.
Definition lreg R x := injective (@mul R x).
Definition rreg R x := injective ((@mul R)^~ x).



The ``field'' characteristic; the definition, and many of the theorems, has to apply to rings as well; indeed, we need the Frobenius automorphism results for a non commutative ring in the proof of Gorenstein 2.6.3.
Definition char (R : Ring.type) of phant R : nat_pred :=
  [pred p | prime p & p%:R == 0 :> R].


Converse ring tag.
Definition converse R : Type := R.

Section RingTheory.

Variable R : ringType.
Implicit Types x y : R.

Lemma mulrA : @associative R *%R.
Lemma mul1r : @left_id R R 1 *%R.
Lemma mulr1 : @right_id R R 1 *%R.
Lemma mulrDl : @left_distributive R R *%R +%R.
Lemma mulrDr : @right_distributive R R *%R +%R.
Lemma oner_neq0 : 1 != 0 :> R.
Lemma oner_eq0 : (1 == 0 :> R) = false.

Lemma mul0r : @left_zero R R 0 *%R.
Lemma mulr0 : @right_zero R R 0 *%R.
Lemma mulrN x y : x × (- y) = - (x × y).
Lemma mulNr x y : (- x) × y = - (x × y).
Lemma mulrNN x y : (- x) × (- y) = x × y.
Lemma mulN1r x : -1 × x = - x.
Lemma mulrN1 x : x × -1 = - x.

Canonical mul_monoid := Monoid.Law mulrA mul1r mulr1.
Canonical muloid := Monoid.MulLaw mul0r mulr0.
Canonical addoid := Monoid.AddLaw mulrDl mulrDr.

Lemma mulr_suml I r P (F : I R) x :
  (\sum_(i <- r | P i) F i) × x = \sum_(i <- r | P i) F i × x.

Lemma mulr_sumr I r P (F : I R) x :
  x × (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x × F i.

Lemma mulrBl x y z : (y - z) × x = y × x - z × x.

Lemma mulrBr x y z : x × (y - z) = x × y - x × z.

Lemma mulrnAl x y n : (x *+ n) × y = (x × y) *+ n.

Lemma mulrnAr x y n : x × (y *+ n) = (x × y) *+ n.

Lemma mulr_natl x n : n%:R × x = x *+ n.

Lemma mulr_natr x n : x × n%:R = x *+ n.

Lemma natrD m n : (m + n)%:R = m%:R + n%:R :> R.

Lemma natr1 n : n%:R + 1 = n.+1%:R :> R.

Lemma nat1r n : 1 + n%:R = n.+1%:R :> R.

Lemma natrB m n : n m (m - n)%:R = m%:R - n%:R :> R.

Definition natr_sum := big_morph (natmul 1) natrD (mulr0n 1).

Lemma natrM m n : (m × n)%:R = m%:R × n%:R :> R.

Lemma expr0 x : x ^+ 0 = 1.
Lemma expr1 x : x ^+ 1 = x.
Lemma expr2 x : x ^+ 2 = x × x.

Lemma exprS x n : x ^+ n.+1 = x × x ^+ n.

Lemma expr0n n : 0 ^+ n = (n == 0%N)%:R :> R.

Lemma expr1n n : 1 ^+ n = 1 :> R.

Lemma exprD x m n : x ^+ (m + n) = x ^+ m × x ^+ n.

Lemma exprSr x n : x ^+ n.+1 = x ^+ n × x.

Lemma expr_sum x (I : Type) (s : seq I) (P : pred I) F :
  x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ F i :> R.

Lemma commr_sym x y : comm x y comm y x.
Lemma commr_refl x : comm x x.

Lemma commr0 x : comm x 0.

Lemma commr1 x : comm x 1.

Lemma commrN x y : comm x y comm x (- y).

Lemma commrN1 x : comm x (-1).

Lemma commrD x y z : comm x y comm x z comm x (y + z).

Lemma commrB x y z : comm x y comm x z comm x (y - z).

Lemma commr_sum (I : Type) (s : seq I) (P : pred I) (F : I R) x :
  ( i, P i comm x (F i)) comm x (\sum_(i <- s | P i) F i).

Lemma commrMn x y n : comm x y comm x (y *+ n).

Lemma commrM x y z : comm x y comm x z comm x (y × z).

Lemma commr_prod (I : Type) (s : seq I) (P : pred I) (F : I R) x :
  ( i, P i comm x (F i)) comm x (\prod_(i <- s | P i) F i).

Lemma commr_nat x n : comm x n%:R.

Lemma commrX x y n : comm x y comm x (y ^+ n).

Lemma exprMn_comm x y n : comm x y (x × y) ^+ n = x ^+ n × y ^+ n.

Lemma commr_sign x n : comm x ((-1) ^+ n).

Lemma exprMn_n x m n : (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.

Lemma exprM x m n : x ^+ (m × n) = x ^+ m ^+ n.

Lemma exprAC x m n : (x ^+ m) ^+ n = (x ^+ n) ^+ m.

Lemma expr_mod n x i : x ^+ n = 1 x ^+ (i %% n) = x ^+ i.

Lemma expr_dvd n x i : x ^+ n = 1 n %| i x ^+ i = 1.

Lemma natrX n k : (n ^ k)%:R = n%:R ^+ k :> R.

Lemma signr_odd n : (-1) ^+ (odd n) = (-1) ^+ n :> R.

Lemma signr_eq0 n : ((-1) ^+ n == 0 :> R) = false.

Lemma mulr_sign (b : bool) x : (-1) ^+ b × x = (if b then - x else x).

Lemma signr_addb b1 b2 : (-1) ^+ (b1 (+) b2) = (-1) ^+ b1 × (-1) ^+ b2 :> R.

Lemma signrE (b : bool) : (-1) ^+ b = 1 - b.*2%:R :> R.

Lemma signrN b : (-1) ^+ (~~ b) = - (-1) ^+ b :> R.

Lemma mulr_signM (b1 b2 : bool) x1 x2 :
  ((-1) ^+ b1 × x1) × ((-1) ^+ b2 × x2) = (-1) ^+ (b1 (+) b2) × (x1 × x2).

Lemma exprNn x n : (- x) ^+ n = (-1) ^+ n × x ^+ n :> R.

Lemma sqrrN x : (- x) ^+ 2 = x ^+ 2.

Lemma sqrr_sign n : ((-1) ^+ n) ^+ 2 = 1 :> R.

Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)).

Lemma lastr_eq0 (s : seq R) x : x != 0 (last x s == 0) = (last 1 s == 0).

Lemma mulrI_eq0 x y : lreg x (x × y == 0) = (y == 0).

Lemma lreg_neq0 x : lreg x x != 0.

Lemma mulrI0_lreg x : ( y, x × y = 0 y = 0) lreg x.

Lemma lregN x : lreg x lreg (- x).

Lemma lreg1 : lreg (1 : R).

Lemma lregM x y : lreg x lreg y lreg (x × y).

Lemma lregMl (a b: R) : lreg (a × b) lreg b.

Lemma rregMr (a b: R) : rreg (a × b) rreg a.

Lemma lregX x n : lreg x lreg (x ^+ n).

Lemma lreg_sign n : lreg ((-1) ^+ n : R).

Lemma iter_mulr n x y : iter n ( *%R x) y = x ^+ n × y.

Lemma iter_mulr_1 n x : iter n ( *%R x) 1 = x ^+ n.

Lemma prodr_const (I : finType) (A : pred I) x : \prod_(i in A) x = x ^+ #|A|.

Lemma prodr_const_nat n m x : \prod_(n i < m) x = x ^+ (m - n).

Lemma prodrXr x I r P (F : I nat) :
  \prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).

Lemma prodrN (I : finType) (A : pred I) (F : I R) :
  \prod_(i in A) - F i = (- 1) ^+ #|A| × \prod_(i in A) F i.

Lemma prodrMn (I : Type) (s : seq I) (P : pred I) (F : I R) (g : I nat) :
  \prod_(i <- s | P i) (F i *+ g i) =
  \prod_(i <- s | P i) (F i) *+ \prod_(i <- s | P i) g i.

Lemma prodrMn_const n (I : finType) (A : pred I) (F : I R) :
  \prod_(i in A) (F i *+ n) = \prod_(i in A) F i *+ n ^ #|A|.

Lemma natr_prod I r P (F : I nat) :
  (\prod_(i <- r | P i) F i)%:R = \prod_(i <- r | P i) (F i)%:R :> R.

Lemma exprDn_comm x y n (cxy : comm x y) :
  (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).

Lemma exprBn_comm x y n (cxy : comm x y) :
  (x - y) ^+ n =
    \sum_(i < n.+1) ((-1) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).

Lemma subrXX_comm x y n (cxy : comm x y) :
  x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).

Lemma exprD1n x n : (x + 1) ^+ n = \sum_(i < n.+1) x ^+ i *+ 'C(n, i).

Lemma subrX1 x n : x ^+ n - 1 = (x - 1) × (\sum_(i < n) x ^+ i).

Lemma sqrrD1 x : (x + 1) ^+ 2 = x ^+ 2 + x *+ 2 + 1.

Lemma sqrrB1 x : (x - 1) ^+ 2 = x ^+ 2 - x *+ 2 + 1.

Lemma subr_sqr_1 x : x ^+ 2 - 1 = (x - 1) × (x + 1).

Definition Frobenius_aut p of p \in [char R] := fun xx ^+ p.

Section FrobeniusAutomorphism.

Variable p : nat.
Hypothesis charFp : p \in [char R].

Lemma charf0 : p%:R = 0 :> R.
Lemma charf_prime : prime p.
Hint Resolve charf_prime : core.

Lemma mulrn_char x : x *+ p = 0.

Lemma natr_mod_char n : (n %% p)%:R = n%:R :> R.

Lemma dvdn_charf n : (p %| n)%N = (n%:R == 0 :> R).

Lemma charf_eq : [char R] =i (p : nat_pred).

Lemma bin_lt_charf_0 k : 0 < k < p 'C(p, k)%:R = 0 :> R.


Lemma Frobenius_autE x : x^f = x ^+ p.

Lemma Frobenius_aut0 : 0^f = 0.

Lemma Frobenius_aut1 : 1^f = 1.

Lemma Frobenius_autD_comm x y (cxy : comm x y) : (x + y)^f = x^f + y^f.

Lemma Frobenius_autMn x n : (x *+ n)^f = x^f *+ n.

Lemma Frobenius_aut_nat n : (n%:R)^f = n%:R.

Lemma Frobenius_autM_comm x y : comm x y (x × y)^f = x^f × y^f.

Lemma Frobenius_autX x n : (x ^+ n)^f = x^f ^+ n.

Lemma Frobenius_autN x : (- x)^f = - x^f.

Lemma Frobenius_autB_comm x y : comm x y (x - y)^f = x^f - y^f.

End FrobeniusAutomorphism.

Lemma exprNn_char x n : [char R].-nat n (- x) ^+ n = - (x ^+ n).

Section Char2.

Hypothesis charR2 : 2 \in [char R].

Lemma addrr_char2 x : x + x = 0.

Lemma oppr_char2 x : - x = x.

Lemma subr_char2 x y : x - y = x + y.

Lemma addrK_char2 x : involutive (+%R^~ x).

Lemma addKr_char2 x : involutive (+%R x).

End Char2.

Canonical converse_eqType := [eqType of R^c].
Canonical converse_choiceType := [choiceType of R^c].
Canonical converse_zmodType := [zmodType of R^c].

Definition converse_ringMixin :=
  let mul' x y := y × x in
  let mulrA' x y z := esym (mulrA z y x) in
  let mulrDl' x y z := mulrDr z x y in
  let mulrDr' x y z := mulrDl y z x in
  @Ring.Mixin converse_zmodType
    1 mul' mulrA' mulr1 mul1r mulrDl' mulrDr' oner_neq0.
Canonical converse_ringType := RingType R^c converse_ringMixin.

Section ClosedPredicates.

Variable S : {pred R}.

Definition mulr_2closed := {in S &, u v, u × v \in S}.
Definition mulr_closed := 1 \in S mulr_2closed.
Definition smulr_closed := -1 \in S mulr_2closed.
Definition semiring_closed := addr_closed S mulr_closed.
Definition subring_closed := [/\ 1 \in S, subr_2closed S & mulr_2closed].

Lemma smulr_closedM : smulr_closed mulr_closed.

Lemma smulr_closedN : smulr_closed oppr_closed S.

Lemma semiring_closedD : semiring_closed addr_closed S.

Lemma semiring_closedM : semiring_closed mulr_closed.

Lemma subring_closedB : subring_closed zmod_closed S.

Lemma subring_closedM : subring_closed smulr_closed.

Lemma subring_closed_semi : subring_closed semiring_closed.

End ClosedPredicates.

End RingTheory.

Section RightRegular.

Variable R : ringType.
Implicit Types x y : R.
Let Rc := converse_ringType R.

Lemma mulIr_eq0 x y : rreg x (y × x == 0) = (y == 0).

Lemma mulIr0_rreg x : ( y, y × x = 0 y = 0) rreg x.

Lemma rreg_neq0 x : rreg x x != 0.

Lemma rregN x : rreg x rreg (- x).

Lemma rreg1 : rreg (1 : R).

Lemma rregM x y : rreg x rreg y rreg (x × y).

Lemma revrX x n : (x : Rc) ^+ n = (x : R) ^+ n.

Lemma rregX x n : rreg x rreg (x ^+ n).

End RightRegular.

Module Lmodule.

Structure mixin_of (R : ringType) (V : zmodType) : Type := Mixin {
  scale : R V V;
  _ : a b v, scale a (scale b v) = scale (a × b) v;
  _ : left_id 1 scale;
  _ : right_distributive scale +%R;
  _ : v, {morph scale^~ v: a b / a + b}
}.

Section ClassDef.

Variable R : ringType.

Record class_of V := Class {
  base : Zmodule.class_of V;
  mixin : mixin_of R (Zmodule.Pack base)
}.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phR T c.

Definition pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0)) :=
  fun bT b & phant_id (Zmodule.class bT) b
  fun m & phant_id m0 mPack phR (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.

End ClassDef.

Module Import Exports.
Coercion base : class_of >-> 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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Notation lmodType R := (type (Phant R)).
Notation LmodType R T m := (@pack _ (Phant R) T _ m _ _ id _ id).
Notation LmodMixin := Mixin.
Notation "[ 'lmodType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'lmodType' R 'of' T 'for' cT ]") : form_scope.
Notation "[ 'lmodType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'lmodType' R 'of' T ]") : form_scope.
End Exports.

End Lmodule.
Import Lmodule.Exports.

Definition scale (R : ringType) (V : lmodType R) : R V V :=
  Lmodule.scale (Lmodule.class V).


Section LmoduleTheory.

Variables (R : ringType) (V : lmodType R).
Implicit Types (a b c : R) (u v : V).


Lemma scalerA a b v : a *: (b *: v) = a × b *: v.

Lemma scale1r : @left_id R V 1 *:%R.

Lemma scalerDr a : {morph *:%R a : u v / u + v}.

Lemma scalerDl v : {morph *:%R^~ v : a b / a + b}.

Lemma scale0r v : 0 *: v = 0.

Lemma scaler0 a : a *: 0 = 0 :> V.

Lemma scaleNr a v : - a *: v = - (a *: v).

Lemma scaleN1r v : (- 1) *: v = - v.

Lemma scalerN a v : a *: (- v) = - (a *: v).

Lemma scalerBl a b v : (a - b) *: v = a *: v - b *: v.

Lemma scalerBr a u v : a *: (u - v) = a *: u - a *: v.

Lemma scaler_nat n v : n%:R *: v = v *+ n.

Lemma scaler_sign (b : bool) v: (-1) ^+ b *: v = (if b then - v else v).

Lemma signrZK n : @involutive V ( *:%R ((-1) ^+ n)).

Lemma scalerMnl a v n : a *: v *+ n = (a *+ n) *: v.

Lemma scalerMnr a v n : a *: v *+ n = a *: (v *+ n).

Lemma scaler_suml v I r (P : pred I) F :
  (\sum_(i <- r | P i) F i) *: v = \sum_(i <- r | P i) F i *: v.

Lemma scaler_sumr a I r (P : pred I) (F : I V) :
  a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.

Section ClosedPredicates.

Variable S : {pred V}.

Definition scaler_closed := a, {in S, v, a *: v \in S}.
Definition linear_closed := a, {in S &, u v, a *: u + v \in S}.
Definition submod_closed := 0 \in S linear_closed.

Lemma linear_closedB : linear_closed subr_2closed S.

Lemma submod_closedB : submod_closed zmod_closed S.

Lemma submod_closedZ : submod_closed scaler_closed.

End ClosedPredicates.

End LmoduleTheory.

Module Lalgebra.

Definition axiom (R : ringType) (V : lmodType R) (mul : V V V) :=
   a u v, a *: mul u v = mul (a *: u) v.

Section ClassDef.

Variable R : ringType.

Record class_of (T : Type) : Type := Class {
  base : Ring.class_of T;
  mixin : Lmodule.mixin_of R (Zmodule.Pack base);
  ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin)) (Ring.mul base)
}.
Definition base2 R m := Lmodule.Class (@mixin R m).

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phR T c.

Definition pack b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0) mul0) :=
  fun bT b & phant_id (Ring.class bT) (b : Ring.class_of T) ⇒
  fun mT m & phant_id (@Lmodule.class R phR mT) (@Lmodule.Class R T b m) ⇒
  fun ax & phant_id axT ax
  Pack (Phant R) (@Class T b m ax).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition lmodType := @Lmodule.Pack R phR cT class.
Definition lmod_ringType := @Lmodule.Pack R phR ringType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Ring.class_of.
Coercion base2 : 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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion lmodType : type >-> Lmodule.type.
Canonical lmodType.
Canonical lmod_ringType.
Notation lalgType R := (type (Phant R)).
Notation LalgType R T a := (@pack _ (Phant R) T _ _ a _ _ id _ _ id _ id).
Notation "[ 'lalgType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'lalgType' R 'of' T 'for' cT ]")
  : form_scope.
Notation "[ 'lalgType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'lalgType' R 'of' T ]") : form_scope.
End Exports.

End Lalgebra.
Import Lalgebra.Exports.

Scalar injection (see the definition of in_alg A below).

Regular ring algebra tag.
Definition regular R : Type := R.

Section LalgebraTheory.

Variables (R : ringType) (A : lalgType R).
Implicit Types x y : A.

Lemma scalerAl k (x y : A) : k *: (x × y) = k *: x × y.

Lemma mulr_algl a x : a%:A × x = a *: x.

Canonical regular_eqType := [eqType of R^o].
Canonical regular_choiceType := [choiceType of R^o].
Canonical regular_zmodType := [zmodType of R^o].
Canonical regular_ringType := [ringType of R^o].

Definition regular_lmodMixin :=
  let mkMixin := @Lmodule.Mixin R regular_zmodType (@mul R) in
  mkMixin (@mulrA R) (@mul1r R) (@mulrDr R) (fun v a bmulrDl a b v).

Canonical regular_lmodType := LmodType R R^o regular_lmodMixin.
Canonical regular_lalgType := LalgType R R^o (@mulrA regular_ringType).

Section ClosedPredicates.

Variable S : {pred A}.

Definition subalg_closed := [/\ 1 \in S, linear_closed S & mulr_2closed S].

Lemma subalg_closedZ : subalg_closed submod_closed S.

Lemma subalg_closedBM : subalg_closed subring_closed S.

End ClosedPredicates.

End LalgebraTheory.

Morphism hierarchy.

Module Additive.

Section ClassDef.

Variables U V : zmodType.

Definition axiom (f : U V) := {morph f : x y / x - y}.

Structure map (phUV : phant (U V)) := Pack {apply; _ : axiom apply}.

Variables (phUV : phant (U V)) (f g : U V) (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axiom cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
  @Pack phUV f fA.

End ClassDef.

Module Exports.
Notation additive f := (axiom f).
Coercion apply : map >-> Funclass.
Notation Additive fA := (Pack (Phant _) fA).
Notation "{ 'additive' fUV }" := (map (Phant fUV))
  (at level 0, format "{ 'additive' fUV }") : type_scope.
Notation "[ 'additive' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
  (at level 0, format "[ 'additive' 'of' f 'as' g ]") : form_scope.
Notation "[ 'additive' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
  (at level 0, format "[ 'additive' 'of' f ]") : form_scope.
End Exports.

End Additive.
Include Additive.Exports. (* Allows GRing.additive to resolve conflicts. *)

Lifted additive operations.
Section LiftedZmod.
Variables (U : Type) (V : zmodType).
Definition null_fun_head (phV : phant V) of U : V := let: Phant := phV in 0.
Definition add_fun (f g : U V) x := f x + g x.
Definition sub_fun (f g : U V) x := f x - g x.
Definition opp_fun (f : U V) x := - f x.
End LiftedZmod.

Lifted multiplication.
Section LiftedRing.
Variables (R : ringType) (T : Type).
Implicit Type f : T R.
Definition mull_fun a f x := a × f x.
Definition mulr_fun a f x := f x × a.
Definition mul_fun f g x := f x × g x.
End LiftedRing.

Lifted linear operations.
Section LiftedScale.
Variables (R : ringType) (U : Type) (V : lmodType R) (A : lalgType R).
Definition scale_fun a (f : U V) x := a *: f x.
Definition in_alg_head (phA : phant A) k : A := let: Phant := phA in k%:A.
End LiftedScale.

Notation null_fun V := (null_fun_head (Phant V)) (only parsing).
The real in_alg notation is declared after GRing.Theory so that at least in Coq 8.2 it gets precedence when GRing.Theory is not imported.


Arguments add_fun {_ _} f g _ /.
Arguments sub_fun {_ _} f g _ /.
Arguments opp_fun {_ _} f _ /.
Arguments mull_fun {_ _} a f _ /.
Arguments mulr_fun {_ _} a f _ /.
Arguments scale_fun {_ _ _} a f _ /.
Arguments mul_fun {_ _} f g _ /.

Section AdditiveTheory.

Section Properties.

Variables (U V : zmodType) (k : unit) (f : {additive U V}).

Lemma raddfB : {morph f : x y / x - y}.

Lemma raddf0 : f 0 = 0.

Lemma raddf_eq0 x : injective f (f x == 0) = (x == 0).

Lemma raddf_inj : ( x, f x = 0 x = 0) injective f.

Lemma raddfN : {morph f : x / - x}.

Lemma raddfD : {morph f : x y / x + y}.

Lemma raddfMn n : {morph f : x / x *+ n}.

Lemma raddfMNn n : {morph f : x / x *- n}.

Lemma raddf_sum I r (P : pred I) E :
  f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).

Lemma can2_additive f' : cancel f f' cancel f' f additive f'.

Lemma bij_additive :
  bijective f exists2 f' : {additive V U}, cancel f f' & cancel f' f.

Fact locked_is_additive : additive (locked_with k (f : U V)).
Canonical locked_additive := Additive locked_is_additive.

End Properties.

Section RingProperties.

Variables (R S : ringType) (f : {additive R S}).

Lemma raddfMnat n x : f (n%:R × x) = n%:R × f x.

Lemma raddfMsign n x : f ((-1) ^+ n × x) = (-1) ^+ n × f x.

Variables (U : lmodType R) (V : lmodType S) (h : {additive U V}).

Lemma raddfZnat n u : h (n%:R *: u) = n%:R *: h u.

Lemma raddfZsign n u : h ((-1) ^+ n *: u) = (-1) ^+ n *: h u.

End RingProperties.

Section AddFun.

Variables (U V W : zmodType) (f g : {additive V W}) (h : {additive U V}).

Fact idfun_is_additive : additive (@idfun U).
Canonical idfun_additive := Additive idfun_is_additive.

Fact comp_is_additive : additive (f \o h).
Canonical comp_additive := Additive comp_is_additive.

Fact opp_is_additive : additive (-%R : U U).
Canonical opp_additive := Additive opp_is_additive.

Fact null_fun_is_additive : additive (\0 : U V).
Canonical null_fun_additive := Additive null_fun_is_additive.

Fact add_fun_is_additive : additive (f \+ g).
Canonical add_fun_additive := Additive add_fun_is_additive.

Fact sub_fun_is_additive : additive (f \- g).
Canonical sub_fun_additive := Additive sub_fun_is_additive.

Fact opp_fun_is_additive : additive (\- g).
Canonical opp_fun_additive := Additive opp_fun_is_additive.

End AddFun.

Section MulFun.

Variables (R : ringType) (U : zmodType).
Variables (a : R) (f : {additive U R}).

Fact mull_fun_is_additive : additive (a \*o f).
Canonical mull_fun_additive := Additive mull_fun_is_additive.

Fact mulr_fun_is_additive : additive (a \o× f).
Canonical mulr_fun_additive := Additive mulr_fun_is_additive.

End MulFun.

Section ScaleFun.

Variables (R : ringType) (U : zmodType) (V : lmodType R).
Variables (a : R) (f : {additive U V}).

Canonical scale_additive := Additive (@scalerBr R V a).
Canonical scale_fun_additive := [additive of a \*: f as f \; *:%R a].

End ScaleFun.

End AdditiveTheory.

Module RMorphism.

Section ClassDef.

Variables R S : ringType.

Definition mixin_of (f : R S) :=
  {morph f : x y / x × y}%R × (f 1 = 1) : Prop.

Record class_of f : Prop := Class {base : additive f; mixin : mixin_of f}.

Structure map (phRS : phant (R S)) := Pack {apply; _ : class_of apply}.
Variables (phRS : phant (R S)) (f g : R S) (cF : map phRS).

Definition class := let: Pack _ c as cF' := cF return class_of cF' in c.

Definition clone fM of phant_id g (apply cF) & phant_id fM class :=
  @Pack phRS f fM.

Definition pack (fM : mixin_of f) :=
  fun (bF : Additive.map phRS) fA & phant_id (Additive.class bF) fA
  Pack phRS (Class fA fM).

Canonical additive := Additive.Pack phRS class.

End ClassDef.

Module Exports.
Notation multiplicative f := (mixin_of f).
Notation rmorphism f := (class_of f).
Coercion base : rmorphism >-> Additive.axiom.
Coercion mixin : rmorphism >-> multiplicative.
Coercion apply : map >-> Funclass.
Notation RMorphism fM := (Pack (Phant _) fM).
Notation AddRMorphism fM := (pack fM id).
Notation "{ 'rmorphism' fRS }" := (map (Phant fRS))
  (at level 0, format "{ 'rmorphism' fRS }") : type_scope.
Notation "[ 'rmorphism' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
  (at level 0, format "[ 'rmorphism' 'of' f 'as' g ]") : form_scope.
Notation "[ 'rmorphism' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
  (at level 0, format "[ 'rmorphism' 'of' f ]") : form_scope.
Coercion additive : map >-> Additive.map.
Canonical additive.
End Exports.

End RMorphism.
Include RMorphism.Exports.

Section RmorphismTheory.

Section Properties.

Variables (R S : ringType) (k : unit) (f : {rmorphism R S}).

Lemma rmorph0 : f 0 = 0.
Lemma rmorphN : {morph f : x / - x}.
Lemma rmorphD : {morph f : x y / x + y}.
Lemma rmorphB : {morph f: x y / x - y}.
Lemma rmorphMn n : {morph f : x / x *+ n}.
Lemma rmorphMNn n : {morph f : x / x *- n}.
Lemma rmorph_sum I r (P : pred I) E :
  f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).
Lemma rmorphMsign n : {morph f : x / (- 1) ^+ n × x}.

Lemma rmorphismP : rmorphism f.
Lemma rmorphismMP : multiplicative f.
Lemma rmorph1 : f 1 = 1.
Lemma rmorphM : {morph f: x y / x × y}.

Lemma rmorph_prod I r (P : pred I) E :
  f (\prod_(i <- r | P i) E i) = \prod_(i <- r | P i) f (E i).

Lemma rmorphX n : {morph f: x / x ^+ n}.

Lemma rmorph_nat n : f n%:R = n%:R.
Lemma rmorphN1 : f (- 1) = (- 1).

Lemma rmorph_sign n : f ((- 1) ^+ n) = (- 1) ^+ n.

Lemma rmorph_char p : p \in [char R] p \in [char S].

Lemma rmorph_eq_nat x n : injective f (f x == n%:R) = (x == n%:R).

Lemma rmorph_eq1 x : injective f (f x == 1) = (x == 1).

Lemma can2_rmorphism f' : cancel f f' cancel f' f rmorphism f'.

Lemma bij_rmorphism :
  bijective f exists2 f' : {rmorphism S R}, cancel f f' & cancel f' f.

Fact locked_is_multiplicative : multiplicative (locked_with k (f : R S)).
Canonical locked_rmorphism := AddRMorphism locked_is_multiplicative.

End Properties.

Section Projections.

Variables (R S T : ringType) (f : {rmorphism S T}) (g : {rmorphism R S}).

Fact idfun_is_multiplicative : multiplicative (@idfun R).
Canonical idfun_rmorphism := AddRMorphism idfun_is_multiplicative.

Fact comp_is_multiplicative : multiplicative (f \o g).
Canonical comp_rmorphism := AddRMorphism comp_is_multiplicative.

End Projections.

Section InAlgebra.

Variables (R : ringType) (A : lalgType R).

Fact in_alg_is_rmorphism : rmorphism (in_alg_loc A).
Canonical in_alg_additive := Additive in_alg_is_rmorphism.
Canonical in_alg_rmorphism := RMorphism in_alg_is_rmorphism.

Lemma in_algE a : in_alg_loc A a = a%:A.

End InAlgebra.

End RmorphismTheory.

Module Scale.

Section ScaleLaw.

Structure law (R : ringType) (V : zmodType) (s : R V V) := Law {
  op : R V V;
  _ : op = s;
  _ : op (-1) =1 -%R;
  _ : a, additive (op a)
}.

Definition mul_law R := Law (erefl *%R) (@mulN1r R) (@mulrBr R).
Definition scale_law R U := Law (erefl *:%R) (@scaleN1r R U) (@scalerBr R U).

Variables (R : ringType) (V : zmodType) (s : R V V) (s_law : law s).

Lemma opE : s_op = s.
Lemma N1op : s_op (-1) =1 -%R.
Fact opB a : additive (s_op a).
Definition op_additive a := Additive (opB a).

Variables (aR : ringType) (nu : {rmorphism aR R}).
Fact comp_opE : nu \; s_op = nu \; s.
Fact compN1op : (nu \; s_op) (-1) =1 -%R.
Definition comp_law : law (nu \; s) := Law comp_opE compN1op (fun aopB _).

End ScaleLaw.

End Scale.

Module Linear.

Section ClassDef.

Variables (R : ringType) (U : lmodType R) (V : zmodType) (s : R V V).
Implicit Type phUV : phant (U V).

Definition axiom (f : U V) (s_law : Scale.law s) of s = s_law :=
   a, {morph f : u v / a *: u + v >-> s a u + v}.
Definition mixin_of (f : U V) :=
   a, {morph f : v / a *: v >-> s a v}.

Record class_of f : Prop := Class {base : additive f; mixin : mixin_of f}.

Lemma class_of_axiom f s_law Ds : @axiom f s_law Ds class_of f.

Structure map (phUV : phant (U V)) := Pack {apply; _ : class_of apply}.

Variables (phUV : phant (U V)) (f g : U V) (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return class_of cF' in c.
Definition clone fL of phant_id g (apply cF) & phant_id fL class :=
  @Pack phUV f fL.

Definition pack (fZ : mixin_of f) :=
  fun (bF : Additive.map phUV) fA & phant_id (Additive.class bF) fA
  Pack phUV (Class fA fZ).

Canonical additive := Additive.Pack phUV class.

Support for right-to-left rewriting with the generic linearZ rule.
Notation mapUV := (map (Phant (U V))).
Definition map_class := mapUV.
Definition map_at (a : R) := mapUV.
Structure map_for a s_a := MapFor {map_for_map : mapUV; _ : s a = s_a}.
Definition unify_map_at a (f : map_at a) := MapFor f (erefl (s a)).
Structure wrapped := Wrap {unwrap : mapUV}.
Definition wrap (f : map_class) := Wrap f.

End ClassDef.

Module Exports.
Canonical Scale.mul_law.
Canonical Scale.scale_law.
Canonical Scale.comp_law.
Canonical Scale.op_additive.
Delimit Scope linear_ring_scope with linR.
Notation "a *: u" := (@Scale.op _ _ *:%R _ a u) : linear_ring_scope.
Notation "a * u" := (@Scale.op _ _ *%R _ a u) : linear_ring_scope.
Notation "a *:^ nu u" := (@Scale.op _ _ (nu \; *:%R) _ a u)
  (at level 40, nu at level 1, format "a *:^ nu u") : linear_ring_scope.
Notation "a *^ nu u" := (@Scale.op _ _ (nu \; *%R) _ a u)
  (at level 40, nu at level 1, format "a *^ nu u") : linear_ring_scope.
Notation scalable_for s f := (mixin_of s f).
Notation scalable f := (scalable_for *:%R f).
Notation linear_for s f := (axiom f (erefl s)).
Notation linear f := (linear_for *:%R f).
Notation scalar f := (linear_for *%R f).
Notation lmorphism_for s f := (class_of s f).
Notation lmorphism f := (lmorphism_for *:%R f).
Coercion class_of_axiom : axiom >-> lmorphism_for.
Coercion base : lmorphism_for >-> Additive.axiom.
Coercion mixin : lmorphism_for >-> scalable.
Coercion apply : map >-> Funclass.
Notation Linear fL := (Pack (Phant _) fL).
Notation AddLinear fZ := (pack fZ id).
Notation "{ 'linear' fUV | s }" := (map s (Phant fUV))
  (at level 0, format "{ 'linear' fUV | s }") : type_scope.
Notation "{ 'linear' fUV }" := {linear fUV | *:%R}
  (at level 0, format "{ 'linear' fUV }") : type_scope.
Notation "{ 'scalar' U }" := {linear U _ | *%R}
  (at level 0, format "{ 'scalar' U }") : type_scope.
Notation "[ 'linear' 'of' f 'as' g ]" := (@clone _ _ _ _ _ f g _ _ idfun id)
  (at level 0, format "[ 'linear' 'of' f 'as' g ]") : form_scope.
Notation "[ 'linear' 'of' f ]" := (@clone _ _ _ _ _ f f _ _ id id)
  (at level 0, format "[ 'linear' 'of' f ]") : form_scope.
Coercion additive : map >-> Additive.map.
Canonical additive.
Support for right-to-left rewriting with the generic linearZ rule.
Coercion map_for_map : map_for >-> map.
Coercion unify_map_at : map_at >-> map_for.
Canonical unify_map_at.
Coercion unwrap : wrapped >-> map.
Coercion wrap : map_class >-> wrapped.
Canonical wrap.
End Exports.

End Linear.
Include Linear.Exports.

Section LinearTheory.

Variable R : ringType.

Section GenericProperties.

Variables (U : lmodType R) (V : zmodType) (s : R V V) (k : unit).
Variable f : {linear U V | s}.

Lemma linear0 : f 0 = 0.
Lemma linearN : {morph f : x / - x}.
Lemma linearD : {morph f : x y / x + y}.
Lemma linearB : {morph f : x y / x - y}.
Lemma linearMn n : {morph f : x / x *+ n}.
Lemma linearMNn n : {morph f : x / x *- n}.
Lemma linear_sum I r (P : pred I) E :
  f (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f (E i).

Lemma linearZ_LR : scalable_for s f.
Lemma linearP a : {morph f : u v / a *: u + v >-> s a u + v}.

Fact locked_is_scalable : scalable_for s (locked_with k (f : U V)).
Canonical locked_linear := AddLinear locked_is_scalable.

End GenericProperties.

Section BidirectionalLinearZ.

Variables (U : lmodType R) (V : zmodType) (s : R V V).

The general form of the linearZ lemma uses some bespoke interfaces to allow right-to-left rewriting when a composite scaling operation such as conjC \; *%R has been expanded, say in a^* * f u. This redex is matched by using the Scale.law interface to recognize a "head" scaling operation h (here *%R), stow away its "scalar" c, then reconcile h c and s a, once s is known, that is, once the Linear.map structure for f has been found. In general, s and a need not be equal to h and c; indeed they need not have the same type! The unification is performed by the unify_map_at default instance for the Linear.map_for U s a h_c sub-interface of Linear.map; the h_c pattern uses the Scale.law structure to insure it is inferred when rewriting right-to-left. The wrap on the rhs allows rewriting f (a *: b *: u) into a *: b *: f u with rewrite !linearZ /= instead of rewrite linearZ /= linearZ /=. Without it, the first rewrite linearZ would produce (a *: apply (map_for_map (@check_map_at .. a f)) (b *: u)%R)%Rlin and matching the second rewrite LHS would bypass the unify_map_at default instance for b, reuse the one for a, and subsequently fail to match the b *: u argument. The extra wrap / unwrap ensures that this can't happen. In the RL direction, the wrap / unwrap will be inserted on the redex side as needed, without causing unnecessary delta-expansion: using an explicit identity function would have Coq normalize the redex to head normal, then reduce the identity to expose the map_for_map projection, and the expanded Linear.map structure would then be exposed in the result. Most of this machinery will be invisible to a casual user, because all the projections and default instances involved are declared as coercions.

Variables (S : ringType) (h : S V V) (h_law : Scale.law h).

Lemma linearZ c a (h_c := Scale.op h_law c) (f : Linear.map_for U s a h_c) u :
  f (a *: u) = h_c (Linear.wrap f u).

End BidirectionalLinearZ.

Section LmodProperties.

Variables (U V : lmodType R) (f : {linear U V}).

Lemma linearZZ : scalable f.
Lemma linearPZ : linear f.

Lemma can2_linear f' : cancel f f' cancel f' f linear f'.

Lemma bij_linear :
  bijective f exists2 f' : {linear V U}, cancel f f' & cancel f' f.

End LmodProperties.

Section ScalarProperties.

Variable (U : lmodType R) (f : {scalar U}).

Lemma scalarZ : scalable_for *%R f.
Lemma scalarP : scalar f.

End ScalarProperties.

Section LinearLmod.

Variables (W U : lmodType R) (V : zmodType) (s : R V V).
Variables (f : {linear U V | s}) (h : {linear W U}).

Lemma idfun_is_scalable : scalable (@idfun U).
Canonical idfun_linear := AddLinear idfun_is_scalable.

Lemma opp_is_scalable : scalable (-%R : U U).
Canonical opp_linear := AddLinear opp_is_scalable.

Lemma comp_is_scalable : scalable_for s (f \o h).
Canonical comp_linear := AddLinear comp_is_scalable.

Variables (s_law : Scale.law s) (g : {linear U V | Scale.op s_law}).
Let Ds : s =1 Scale.op s_law.

Lemma null_fun_is_scalable : scalable_for (Scale.op s_law) (\0 : U V).
Canonical null_fun_linear := AddLinear null_fun_is_scalable.

Lemma add_fun_is_scalable : scalable_for s (f \+ g).
Canonical add_fun_linear := AddLinear add_fun_is_scalable.

Lemma sub_fun_is_scalable : scalable_for s (f \- g).
Canonical sub_fun_linear := AddLinear sub_fun_is_scalable.

Lemma opp_fun_is_scalable : scalable_for s (\- g).
Canonical opp_fun_linear := AddLinear opp_fun_is_scalable.

End LinearLmod.

Section LinearLalg.

Variables (A : lalgType R) (U : lmodType R).

Variables (a : A) (f : {linear U A}).

Fact mulr_fun_is_scalable : scalable (a \o× f).
Canonical mulr_fun_linear := AddLinear mulr_fun_is_scalable.

End LinearLalg.

End LinearTheory.

Module LRMorphism.

Section ClassDef.

Variables (R : ringType) (A : lalgType R) (B : ringType) (s : R B B).

Record class_of (f : A B) : Prop :=
  Class {base : rmorphism f; mixin : scalable_for s f}.
Definition base2 f (fLM : class_of f) := Linear.Class fLM (mixin fLM).

Structure map (phAB : phant (A B)) := Pack {apply; _ : class_of apply}.

Variables (phAB : phant (A B)) (f : A B) (cF : map phAB).
Definition class := let: Pack _ c as cF' := cF return class_of cF' in c.

Definition clone :=
  fun (g : RMorphism.map phAB) fM & phant_id (RMorphism.class g) fM
  fun (h : Linear.map s phAB) fZ &
     phant_id (Linear.mixin (Linear.class h)) fZ
  Pack phAB (@Class f fM fZ).

Definition pack (fZ : scalable_for s f) :=
  fun (g : RMorphism.map phAB) fM & phant_id (RMorphism.class g) fM
  Pack phAB (Class fM fZ).

Canonical additive := Additive.Pack phAB class.
Canonical rmorphism := RMorphism.Pack phAB class.
Canonical linear := Linear.Pack phAB class.
Canonical join_rmorphism := @RMorphism.Pack _ _ phAB linear class.
Canonical join_linear := @Linear.Pack R A B s phAB rmorphism class.

End ClassDef.

Module Exports.
Notation lrmorphism_for s f := (class_of s f).
Notation lrmorphism f := (lrmorphism_for *:%R f).
Coercion base : lrmorphism_for >-> RMorphism.class_of.
Coercion base2 : lrmorphism_for >-> lmorphism_for.
Coercion apply : map >-> Funclass.
Notation LRMorphism f_lrM := (Pack (Phant _) (Class f_lrM f_lrM)).
Notation AddLRMorphism fZ := (pack fZ id).
Notation "{ 'lrmorphism' fAB | s }" := (map s (Phant fAB))
  (at level 0, format "{ 'lrmorphism' fAB | s }") : type_scope.
Notation "{ 'lrmorphism' fAB }" := {lrmorphism fAB | *:%R}
  (at level 0, format "{ 'lrmorphism' fAB }") : type_scope.
Notation "[ 'lrmorphism' 'of' f ]" := (@clone _ _ _ _ _ f _ _ id _ _ id)
  (at level 0, format "[ 'lrmorphism' 'of' f ]") : form_scope.
Coercion additive : map >-> Additive.map.
Canonical additive.
Coercion rmorphism : map >-> RMorphism.map.
Canonical rmorphism.
Coercion linear : map >-> Linear.map.
Canonical linear.
Canonical join_rmorphism.
Canonical join_linear.
End Exports.

End LRMorphism.
Include LRMorphism.Exports.

Section LRMorphismTheory.

Variables (R : ringType) (A B : lalgType R) (C : ringType) (s : R C C).
Variables (k : unit) (f : {lrmorphism A B}) (g : {lrmorphism B C | s}).

Definition idfun_lrmorphism := [lrmorphism of @idfun A].
Definition comp_lrmorphism := [lrmorphism of g \o f].
Definition locked_lrmorphism := [lrmorphism of locked_with k (f : A B)].

Lemma rmorph_alg a : f a%:A = a%:A.

Lemma lrmorphismP : lrmorphism f.

Lemma can2_lrmorphism f' : cancel f f' cancel f' f lrmorphism f'.

Lemma bij_lrmorphism :
  bijective f exists2 f' : {lrmorphism B A}, cancel f f' & cancel f' f.

End LRMorphismTheory.

Module ComRing.

Definition RingMixin R one mul mulA mulC mul1x mul_addl :=
  let mulx1 := Monoid.mulC_id mulC mul1x in
  let mul_addr := Monoid.mulC_dist mulC mul_addl in
  @Ring.EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr.

Section ClassDef.

Record class_of R :=
  Class {base : Ring.class_of R; mixin : commutative (Ring.mul base)}.

Structure type := Pack {sort; _ : class_of sort}.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack mul0 (m0 : @commutative T T mul0) :=
  fun bT b & phant_id (Ring.class bT) b
  fun m & phant_id m0 mPack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Ring.class_of.
Arguments mixin [R].
Coercion mixin : class_of >-> commutative.
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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Notation comRingType := type.
Notation ComRingType T m := (@pack T _ m _ _ id _ id).
Notation ComRingMixin := RingMixin.
Notation "[ 'comRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'comRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'comRingType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'comRingType' 'of' T ]") : form_scope.
End Exports.

End ComRing.
Import ComRing.Exports.

Section ComRingTheory.

Variable R : comRingType.
Implicit Types x y : R.

Lemma mulrC : @commutative R R *%R.
Canonical mul_comoid := Monoid.ComLaw mulrC.
Lemma mulrCA : @left_commutative R R *%R.
Lemma mulrAC : @right_commutative R R *%R.
Lemma mulrACA : @interchange R *%R *%R.

Lemma exprMn n : {morph (fun xx ^+ n) : x y / x × y}.

Lemma prodrXl n I r (P : pred I) (F : I R) :
  \prod_(i <- r | P i) F i ^+ n = (\prod_(i <- r | P i) F i) ^+ n.

Lemma prodr_undup_exp_count (I : eqType) r (P : pred I) (F : I R) :
  \prod_(i <- undup r | P i) F i ^+ count_mem i r = \prod_(i <- r | P i) F i.

Lemma exprDn x y n :
  (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) × y ^+ i) *+ 'C(n, i).

Lemma exprBn x y n :
  (x - y) ^+ n =
     \sum_(i < n.+1) ((-1) ^+ i × x ^+ (n - i) × y ^+ i) *+ 'C(n, i).

Lemma subrXX x y n :
  x ^+ n - y ^+ n = (x - y) × (\sum_(i < n) x ^+ (n.-1 - i) × y ^+ i).

Lemma sqrrD x y : (x + y) ^+ 2 = x ^+ 2 + x × y *+ 2 + y ^+ 2.

Lemma sqrrB x y : (x - y) ^+ 2 = x ^+ 2 - x × y *+ 2 + y ^+ 2.

Lemma subr_sqr x y : x ^+ 2 - y ^+ 2 = (x - y) × (x + y).

Lemma subr_sqrDB x y : (x + y) ^+ 2 - (x - y) ^+ 2 = x × y *+ 4.

Section FrobeniusAutomorphism.

Variables (p : nat) (charRp : p \in [char R]).

Lemma Frobenius_aut_is_rmorphism : rmorphism (Frobenius_aut charRp).

Canonical Frobenius_aut_additive := Additive Frobenius_aut_is_rmorphism.
Canonical Frobenius_aut_rmorphism := RMorphism Frobenius_aut_is_rmorphism.

End FrobeniusAutomorphism.

Lemma exprDn_char x y n : [char R].-nat n (x + y) ^+ n = x ^+ n + y ^+ n.

Lemma rmorph_comm (S : ringType) (f : {rmorphism R S}) x y :
  comm (f x) (f y).

Section ScaleLinear.

Variables (U V : lmodType R) (b : R) (f : {linear U V}).

Lemma scale_is_scalable : scalable ( *:%R b : V V).
Canonical scale_linear := AddLinear scale_is_scalable.

Lemma scale_fun_is_scalable : scalable (b \*: f).
Canonical scale_fun_linear := AddLinear scale_fun_is_scalable.

End ScaleLinear.

End ComRingTheory.

Module Algebra.

Section Mixin.

Variables (R : ringType) (A : lalgType R).

Definition axiom := k (x y : A), k *: (x × y) = x × (k *: y).

Lemma comm_axiom : phant A commutative (@mul A) axiom.

End Mixin.

Section ClassDef.

Variable R : ringType.

Record class_of (T : Type) : Type := Class {
  base : Lalgebra.class_of R T;
  mixin : axiom (Lalgebra.Pack _ base)
}.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phR T c.

Definition pack b0 (ax0 : @axiom R b0) :=
  fun bT b & phant_id (@Lalgebra.class R phR bT) b
  fun ax & phant_id ax0 axPack phR (@Class T b ax).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition lmodType := @Lmodule.Pack R phR cT class.
Definition lalgType := @Lalgebra.Pack R phR cT class.

End ClassDef.

Module Exports.
Coercion base : 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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion lmodType : type >-> Lmodule.type.
Canonical lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical lalgType.
Notation algType R := (type (Phant R)).
Notation AlgType R A ax := (@pack _ (Phant R) A _ ax _ _ id _ id).
Notation CommAlgType R A := (AlgType R A (comm_axiom (Phant A) (@mulrC _))).
Notation "[ 'algType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'algType' R 'of' T 'for' cT ]")
  : form_scope.
Notation "[ 'algType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'algType' R 'of' T ]") : form_scope.
End Exports.

End Algebra.
Import Algebra.Exports.

Module ComAlgebra.

Section ClassDef.

Variable R : ringType.

Record class_of (T : Type) : Type := Class {
  base : Algebra.class_of R T;
  mixin : commutative (Ring.mul base)
}.
Definition base2 R m := ComRing.Class (@mixin R m).

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.

Definition pack :=
  fun bT b & phant_id (@Algebra.class R phR bT) (b : Algebra.class_of R T) ⇒
  fun mT m & phant_id (ComRing.mixin (ComRing.class mT)) m
  Pack (Phant R) (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition lmodType := @Lmodule.Pack R phR cT class.
Definition lalgType := @Lalgebra.Pack R phR cT class.
Definition algType := @Algebra.Pack R phR cT class.
Definition lmod_comRingType := @Lmodule.Pack R phR comRingType class.
Definition lalg_comRingType := @Lalgebra.Pack R phR comRingType class.
Definition alg_comRingType := @Algebra.Pack R phR comRingType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Algebra.class_of.
Coercion base2 : class_of >-> ComRing.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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion lmodType : type >-> Lmodule.type.
Canonical lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical lalgType.
Coercion algType : type >-> Algebra.type.
Canonical algType.
Canonical lmod_comRingType.
Canonical lalg_comRingType.
Canonical alg_comRingType.

Notation comAlgType R := (type (Phant R)).
Notation "[ 'comAlgType' R 'of' T ]" := (@pack _ (Phant R) T _ _ id _ _ id)
  (at level 0, format "[ 'comAlgType' R 'of' T ]") : form_scope.
End Exports.

End ComAlgebra.
Import ComAlgebra.Exports.

Section AlgebraTheory.

Variables (R : comRingType) (A : algType R).
Implicit Types (k : R) (x y : A).

Lemma scalerAr k x y : k *: (x × y) = x × (k *: y).

Lemma scalerCA k x y : k *: x × y = x × (k *: y).

Lemma mulr_algr a x : x × a%:A = a *: x.

Lemma comm_alg a x : comm a%:A x.

Lemma exprZn k x n : (k *: x) ^+ n = k ^+ n *: x ^+ n.

Lemma scaler_prod I r (P : pred I) (F : I R) (G : I A) :
  \prod_(i <- r | P i) (F i *: G i) =
    \prod_(i <- r | P i) F i *: \prod_(i <- r | P i) G i.

Lemma scaler_prodl (I : finType) (S : pred I) (F : I A) k :
  \prod_(i in S) (k *: F i) = k ^+ #|S| *: \prod_(i in S) F i.

Lemma scaler_prodr (I : finType) (S : pred I) (F : I R) x :
  \prod_(i in S) (F i *: x) = \prod_(i in S) F i *: x ^+ #|S|.

Canonical regular_comRingType := [comRingType of R^o].
Canonical regular_algType := CommAlgType R R^o.
Canonical regular_comAlgType := [comAlgType R of R^o].

Variables (U : lmodType R) (a : A) (f : {linear U A}).

Lemma mull_fun_is_scalable : scalable (a \*o f).
Canonical mull_fun_linear := AddLinear mull_fun_is_scalable.

End AlgebraTheory.

Module UnitRing.

Record mixin_of (R : ringType) : Type := Mixin {
  unit : pred R;
  inv : R R;
  _ : {in unit, left_inverse 1 inv *%R};
  _ : {in unit, right_inverse 1 inv *%R};
  _ : x y, y × x = 1 x × y = 1 unit x;
  _ : {in [predC unit], inv =1 id}
}.

Definition EtaMixin R unit inv mulVr mulrV unitP inv_out :=
  let _ := @Mixin R unit inv mulVr mulrV unitP inv_out in
  @Mixin (Ring.Pack (Ring.class R)) unit inv mulVr mulrV unitP inv_out.

Section ClassDef.

Record class_of (R : Type) : Type := Class {
  base : Ring.class_of R;
  mixin : mixin_of (Ring.Pack base)
}.

Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0)) :=
  fun bT b & phant_id (Ring.class bT) b
  fun m & phant_id m0 mPack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Ring.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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Notation unitRingType := type.
Notation UnitRingType T m := (@pack T _ m _ _ id _ id).
Notation UnitRingMixin := EtaMixin.
Notation "[ 'unitRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'unitRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'unitRingType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'unitRingType' 'of' T ]") : form_scope.
End Exports.

End UnitRing.
Import UnitRing.Exports.

Definition unit {R : unitRingType} :=
  [qualify a u : R | UnitRing.unit (UnitRing.class R) u].
Fact unit_key R : pred_key (@unit R).
Canonical unit_keyed R := KeyedQualifier (@unit_key R).
Definition inv {R : unitRingType} : R R := UnitRing.inv (UnitRing.class R).


Section UnitRingTheory.

Variable R : unitRingType.
Implicit Types x y : R.

Lemma divrr : {in unit, right_inverse 1 (@inv R) *%R}.
Definition mulrV := divrr.

Lemma mulVr : {in unit, left_inverse 1 (@inv R) *%R}.

Lemma invr_out x : x \isn't a unit x^-1 = x.

Lemma unitrP x : reflect ( y, y × x = 1 x × y = 1) (x \is a unit).

Lemma mulKr : {in unit, left_loop (@inv R) *%R}.

Lemma mulVKr : {in unit, rev_left_loop (@inv R) *%R}.

Lemma mulrK : {in unit, right_loop (@inv R) *%R}.

Lemma mulrVK : {in unit, rev_right_loop (@inv R) *%R}.
Definition divrK := mulrVK.

Lemma mulrI : {in @unit R, right_injective *%R}.

Lemma mulIr : {in @unit R, left_injective *%R}.

Due to noncommutativity, fractions are inverted.
Lemma telescope_prodr n m (f : nat R) :
    ( k, n < k < m f k \is a unit) n < m
  \prod_(n k < m) (f k / f k.+1) = f n / f m.

Lemma telescope_prodr_eq n m (f u : nat R) : n < m
    ( k, n < k < m f k \is a unit)
    ( k, (n k < m)%N u k = f k / f k.+1)
  \prod_(n k < m) u k = f n / f m.

Lemma commrV x y : comm x y comm x y^-1.

Lemma unitrE x : (x \is a unit) = (x / x == 1).

Lemma invrK : involutive (@inv R).

Lemma invr_inj : injective (@inv R).

Lemma unitrV x : (x^-1 \in unit) = (x \in unit).

Lemma unitr1 : 1 \in @unit R.

Lemma invr1 : 1^-1 = 1 :> R.

Lemma div1r x : 1 / x = x^-1.
Lemma divr1 x : x / 1 = x.

Lemma natr_div m d :
  d %| m d%:R \is a @unit R (m %/ d)%:R = m%:R / d%:R :> R.

Lemma divrI : {in unit, right_injective (fun x yx / y)}.

Lemma divIr : {in unit, left_injective (fun x yx / y)}.

Lemma unitr0 : (0 \is a @unit R) = false.

Lemma invr0 : 0^-1 = 0 :> R.

Lemma unitrN1 : -1 \is a @unit R.

Lemma invrN1 : (-1)^-1 = -1 :> R.

Lemma invr_sign n : ((-1) ^- n) = (-1) ^+ n :> R.

Lemma unitrMl x y : y \is a unit (x × y \is a unit) = (x \is a unit).

Lemma unitrMr x y : x \is a unit (x × y \is a unit) = (y \is a unit).

Lemma invrM : {in unit &, x y, (x × y)^-1 = y^-1 × x^-1}.

Lemma unitrM_comm x y :
  comm x y (x × y \is a unit) = (x \is a unit) && (y \is a unit).

Lemma unitrX x n : x \is a unit x ^+ n \is a unit.

Lemma unitrX_pos x n : n > 0 (x ^+ n \in unit) = (x \in unit).

Lemma exprVn x n : x^-1 ^+ n = x ^- n.

Lemma exprB m n x : n m x \is a unit x ^+ (m - n) = x ^+ m / x ^+ n.

Lemma invr_neq0 x : x != 0 x^-1 != 0.

Lemma invr_eq0 x : (x^-1 == 0) = (x == 0).

Lemma invr_eq1 x : (x^-1 == 1) = (x == 1).

Lemma rev_unitrP (x y : R^c) : y × x = 1 x × y = 1 x \is a unit.

Definition converse_unitRingMixin :=
  @UnitRing.Mixin _ (unit : {pred R^c}) _ mulrV mulVr rev_unitrP invr_out.
Canonical converse_unitRingType := UnitRingType R^c converse_unitRingMixin.
Canonical regular_unitRingType := [unitRingType of R^o].

Section ClosedPredicates.

Variables S : {pred R}.

Definition invr_closed := {in S, x, x^-1 \in S}.
Definition divr_2closed := {in S &, x y, x / y \in S}.
Definition divr_closed := 1 \in S divr_2closed.
Definition sdivr_closed := -1 \in S divr_2closed.
Definition divring_closed := [/\ 1 \in S, subr_2closed S & divr_2closed].

Lemma divr_closedV : divr_closed invr_closed.

Lemma divr_closedM : divr_closed mulr_closed S.

Lemma sdivr_closed_div : sdivr_closed divr_closed.

Lemma sdivr_closedM : sdivr_closed smulr_closed S.

Lemma divring_closedBM : divring_closed subring_closed S.

Lemma divring_closed_div : divring_closed sdivr_closed.

End ClosedPredicates.

End UnitRingTheory.

Arguments invrK {R}.
Arguments invr_inj {R} [x1 x2].
Arguments telescope_prodr_eq {R n m} f u.

Section UnitRingMorphism.

Variables (R S : unitRingType) (f : {rmorphism R S}).

Lemma rmorph_unit x : x \in unit f x \in unit.

Lemma rmorphV : {in unit, {morph f: x / x^-1}}.

Lemma rmorph_div x y : y \in unit f (x / y) = f x / f y.

End UnitRingMorphism.

Module ComUnitRing.

Section Mixin.

Variables (R : comRingType) (unit : pred R) (inv : R R).
Hypothesis mulVx : {in unit, left_inverse 1 inv *%R}.
Hypothesis unitPl : x y, y × x = 1 unit x.

Fact mulC_mulrV : {in unit, right_inverse 1 inv *%R}.

Fact mulC_unitP x y : y × x = 1 x × y = 1 unit x.

Definition Mixin := UnitRingMixin mulVx mulC_mulrV mulC_unitP.

End Mixin.

Section ClassDef.

Record class_of (R : Type) : Type := Class {
  base : ComRing.class_of R;
  mixin : UnitRing.mixin_of (Ring.Pack base)
}.
Definition base2 R m := UnitRing.Class (@mixin R m).

Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.

Definition pack :=
  fun bT b & phant_id (ComRing.class bT) (b : ComRing.class_of T) ⇒
  fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) ⇒
  Pack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition com_unitRingType := @UnitRing.Pack comRingType class.

End ClassDef.

Module Import Exports.
Coercion base : class_of >-> ComRing.class_of.
Coercion mixin : class_of >-> UnitRing.mixin_of.
Coercion base2 : 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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Canonical com_unitRingType.
Notation comUnitRingType := type.
Notation ComUnitRingMixin := Mixin.
Notation "[ 'comUnitRingType' 'of' T ]" := (@pack T _ _ id _ _ id)
  (at level 0, format "[ 'comUnitRingType' 'of' T ]") : form_scope.
End Exports.

End ComUnitRing.
Import ComUnitRing.Exports.

Module UnitAlgebra.

Section ClassDef.

Variable R : ringType.

Record class_of (T : Type) : Type := Class {
  base : Algebra.class_of R T;
  mixin : GRing.UnitRing.mixin_of (Ring.Pack base)
}.
Definition base2 R m := UnitRing.Class (@mixin R m).

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.

Definition pack :=
  fun bT b & phant_id (@Algebra.class R phR bT) (b : Algebra.class_of R T) ⇒
  fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m
  Pack (Phant R) (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition lmodType := @Lmodule.Pack R phR cT class.
Definition lalgType := @Lalgebra.Pack R phR cT class.
Definition algType := @Algebra.Pack R phR cT class.
Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType class.
Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType class.
Definition alg_unitRingType := @Algebra.Pack R phR unitRingType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Algebra.class_of.
Coercion base2 : 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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Coercion lmodType : type >-> Lmodule.type.
Canonical lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical lalgType.
Coercion algType : type >-> Algebra.type.
Canonical algType.
Canonical lmod_unitRingType.
Canonical lalg_unitRingType.
Canonical alg_unitRingType.
Notation unitAlgType R := (type (Phant R)).
Notation "[ 'unitAlgType' R 'of' T ]" := (@pack _ (Phant R) T _ _ id _ _ id)
  (at level 0, format "[ 'unitAlgType' R 'of' T ]") : form_scope.
End Exports.

End UnitAlgebra.
Import UnitAlgebra.Exports.

Module ComUnitAlgebra.

Section ClassDef.

Variable R : ringType.

Record class_of (T : Type) : Type := Class {
  base : ComAlgebra.class_of R T;
  mixin : GRing.UnitRing.mixin_of (ComRing.Pack base)
}.
Definition base2 R m := UnitAlgebra.Class (@mixin R m).
Definition base3 R m := ComUnitRing.Class (@mixin R m).

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.

Definition pack :=
  fun bT b & phant_id (@ComAlgebra.class R phR bT) (b : ComAlgebra.class_of R T) ⇒
  fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m
  Pack (Phant R) (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition comUnitRingType := @ComUnitRing.Pack cT class.
Definition lmodType := @Lmodule.Pack R phR cT class.
Definition lalgType := @Lalgebra.Pack R phR cT class.
Definition algType := @Algebra.Pack R phR cT class.
Definition comAlgType := @ComAlgebra.Pack R phR cT class.
Definition unitAlgType := @UnitAlgebra.Pack R phR cT class.
Definition comalg_unitRingType := @ComAlgebra.Pack R phR unitRingType class.
Definition comalg_comUnitRingType :=
  @ComAlgebra.Pack R phR comUnitRingType class.
Definition comalg_unitAlgType := @ComAlgebra.Pack R phR unitAlgType class.
Definition unitalg_comRingType := @UnitAlgebra.Pack R phR comRingType class.
Definition unitalg_comUnitRingType :=
  @UnitAlgebra.Pack R phR comUnitRingType class.
Definition lmod_comUnitRingType := @Lmodule.Pack R phR comUnitRingType class.
Definition lalg_comUnitRingType := @Lalgebra.Pack R phR comUnitRingType class.
Definition alg_comUnitRingType := @Algebra.Pack R phR comUnitRingType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> ComAlgebra.class_of.
Coercion base2 : class_of >-> UnitAlgebra.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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical comUnitRingType.
Coercion lmodType : type >-> Lmodule.type.
Canonical lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical lalgType.
Coercion algType : type >-> Algebra.type.
Canonical algType.
Coercion comAlgType : type >-> ComAlgebra.type.
Canonical comAlgType.
Coercion unitAlgType : type >-> UnitAlgebra.type.
Canonical unitAlgType.
Canonical comalg_unitRingType.
Canonical comalg_comUnitRingType.
Canonical comalg_unitAlgType.
Canonical unitalg_comRingType.
Canonical unitalg_comUnitRingType.
Canonical lmod_comUnitRingType.
Canonical lalg_comUnitRingType.
Canonical alg_comUnitRingType.

Notation comUnitAlgType R := (type (Phant R)).
Notation "[ 'comUnitAlgType' R 'of' T ]" := (@pack _ (Phant R) T _ _ id _ _ id)
  (at level 0, format "[ 'comUnitAlgType' R 'of' T ]") : form_scope.
End Exports.

End ComUnitAlgebra.
Import ComUnitAlgebra.Exports.

Section ComUnitRingTheory.

Variable R : comUnitRingType.
Implicit Types x y : R.

Lemma unitrM x y : (x × y \in unit) = (x \in unit) && (y \in unit).

Lemma unitrPr x : reflect ( y, x × y = 1) (x \in unit).

Lemma mulr1_eq x y : x × y = 1 x^-1 = y.

Lemma divr1_eq x y : x / y = 1 x = y.

Lemma divKr x : x \is a unit {in unit, involutive (fun yx / y)}.

Lemma expr_div_n x y n : (x / y) ^+ n = x ^+ n / y ^+ n.

Canonical regular_comUnitRingType := [comUnitRingType of R^o].
Canonical regular_unitAlgType := [unitAlgType R of R^o].
Canonical regular_comUnitAlgType := [comUnitAlgType R of R^o].

End ComUnitRingTheory.

Section UnitAlgebraTheory.

Variable (R : comUnitRingType) (A : unitAlgType R).
Implicit Types (k : R) (x y : A).

Lemma scaler_injl : {in unit, @right_injective R A A *:%R}.

Lemma scaler_unit k x : k \in unit (k *: x \in unit) = (x \in unit).

Lemma invrZ k x : k \in unit x \in unit (k *: x)^-1 = k^-1 *: x^-1.

Section ClosedPredicates.

Variables S : {pred A}.

Definition divalg_closed := [/\ 1 \in S, linear_closed S & divr_2closed S].

Lemma divalg_closedBdiv : divalg_closed divring_closed S.

Lemma divalg_closedZ : divalg_closed subalg_closed S.

End ClosedPredicates.

End UnitAlgebraTheory.

Interface structures for algebraically closed predicates.
Module Pred.

Structure opp V S := Opp {opp_key : pred_key S; _ : @oppr_closed V S}.
Structure add V S := Add {add_key : pred_key S; _ : @addr_closed V S}.
Structure mul R S := Mul {mul_key : pred_key S; _ : @mulr_closed R S}.
Structure zmod V S := Zmod {zmod_add : add S; _ : @oppr_closed V S}.
Structure semiring R S := Semiring {semiring_add : add S; _ : @mulr_closed R S}.
Structure smul R S := Smul {smul_opp : opp S; _ : @mulr_closed R S}.
Structure div R S := Div {div_mul : mul S; _ : @invr_closed R S}.
Structure submod R V S :=
  Submod {submod_zmod : zmod S; _ : @scaler_closed R V S}.
Structure subring R S := Subring {subring_zmod : zmod S; _ : @mulr_closed R S}.
Structure sdiv R S := Sdiv {sdiv_smul : smul S; _ : @invr_closed R S}.
Structure subalg (R : ringType) (A : lalgType R) S :=
  Subalg {subalg_ring : subring S; _ : @scaler_closed R A S}.
Structure divring R S :=
  Divring {divring_ring : subring S; _ : @invr_closed R S}.
Structure divalg (R : ringType) (A : unitAlgType R) S :=
  Divalg {divalg_ring : divring S; _ : @scaler_closed R A S}.

Section Subtyping.

Ltac done := case⇒ *; assumption.
Fact zmod_oppr R S : @zmod R S oppr_closed S.
Fact semiring_mulr R S : @semiring R S mulr_closed S.
Fact smul_mulr R S : @smul R S mulr_closed S.
Fact submod_scaler R V S : @submod R V S scaler_closed S.
Fact subring_mulr R S : @subring R S mulr_closed S.
Fact sdiv_invr R S : @sdiv R S invr_closed S.
Fact subalg_scaler R A S : @subalg R A S scaler_closed S.
Fact divring_invr R S : @divring R S invr_closed S.
Fact divalg_scaler R A S : @divalg R A S scaler_closed S.

Definition zmod_opp R S (addS : @zmod R S) :=
  Opp (add_key (zmod_add addS)) (zmod_oppr addS).
Definition semiring_mul R S (ringS : @semiring R S) :=
  Mul (add_key (semiring_add ringS)) (semiring_mulr ringS).
Definition smul_mul R S (mulS : @smul R S) :=
  Mul (opp_key (smul_opp mulS)) (smul_mulr mulS).
Definition subring_semi R S (ringS : @subring R S) :=
  Semiring (zmod_add (subring_zmod ringS)) (subring_mulr ringS).
Definition subring_smul R S (ringS : @subring R S) :=
  Smul (zmod_opp (subring_zmod ringS)) (subring_mulr ringS).
Definition sdiv_div R S (divS : @sdiv R S) :=
  Div (smul_mul (sdiv_smul divS)) (sdiv_invr divS).
Definition subalg_submod R A S (algS : @subalg R A S) :=
  Submod (subring_zmod (subalg_ring algS)) (subalg_scaler algS).
Definition divring_sdiv R S (ringS : @divring R S) :=
  Sdiv (subring_smul (divring_ring ringS)) (divring_invr ringS).
Definition divalg_alg R A S (algS : @divalg R A S) :=
  Subalg (divring_ring (divalg_ring algS)) (divalg_scaler algS).

End Subtyping.

Section Extensionality.
This could be avoided by exploiting the Coq 8.4 eta-convertibility.

Lemma opp_ext (U : zmodType) S k (kS : @keyed_pred U S k) :
  oppr_closed kS oppr_closed S.

Lemma add_ext (U : zmodType) S k (kS : @keyed_pred U S k) :
  addr_closed kS addr_closed S.

Lemma mul_ext (R : ringType) S k (kS : @keyed_pred R S k) :
  mulr_closed kS mulr_closed S.

Lemma scale_ext (R : ringType) (U : lmodType R) S k (kS : @keyed_pred U S k) :
  scaler_closed kS scaler_closed S.

Lemma inv_ext (R : unitRingType) S k (kS : @keyed_pred R S k) :
  invr_closed kS invr_closed S.

End Extensionality.

Module Default.
Definition opp V S oppS := @Opp V S (DefaultPredKey S) oppS.
Definition add V S addS := @Add V S (DefaultPredKey S) addS.
Definition mul R S mulS := @Mul R S (DefaultPredKey S) mulS.
Definition zmod V S addS oppS := @Zmod V S (add addS) oppS.
Definition semiring R S addS mulS := @Semiring R S (add addS) mulS.
Definition smul R S oppS mulS := @Smul R S (opp oppS) mulS.
Definition div R S mulS invS := @Div R S (mul mulS) invS.
Definition submod R V S addS oppS linS := @Submod R V S (zmod addS oppS) linS.
Definition subring R S addS oppS mulS := @Subring R S (zmod addS oppS) mulS.
Definition sdiv R S oppS mulS invS := @Sdiv R S (smul oppS mulS) invS.
Definition subalg R A S addS oppS mulS linS :=
  @Subalg R A S (subring addS oppS mulS) linS.
Definition divring R S addS oppS mulS invS :=
  @Divring R S (subring addS oppS mulS) invS.
Definition divalg R A S addS oppS mulS invS linS :=
  @Divalg R A S (divring addS oppS mulS invS) linS.
End Default.

Module Exports.

Notation oppr_closed := oppr_closed.
Notation addr_closed := addr_closed.
Notation mulr_closed := mulr_closed.
Notation zmod_closed := zmod_closed.
Notation smulr_closed := smulr_closed.
Notation invr_closed := invr_closed.
Notation divr_closed := divr_closed.
Notation scaler_closed := scaler_closed.
Notation linear_closed := linear_closed.
Notation submod_closed := submod_closed.
Notation semiring_closed := semiring_closed.
Notation subring_closed := subring_closed.
Notation sdivr_closed := sdivr_closed.
Notation subalg_closed := subalg_closed.
Notation divring_closed := divring_closed.
Notation divalg_closed := divalg_closed.

Coercion zmod_closedD : zmod_closed >-> addr_closed.
Coercion zmod_closedN : zmod_closed >-> oppr_closed.
Coercion smulr_closedN : smulr_closed >-> oppr_closed.
Coercion smulr_closedM : smulr_closed >-> mulr_closed.
Coercion divr_closedV : divr_closed >-> invr_closed.
Coercion divr_closedM : divr_closed >-> mulr_closed.
Coercion submod_closedZ : submod_closed >-> scaler_closed.
Coercion submod_closedB : submod_closed >-> zmod_closed.
Coercion semiring_closedD : semiring_closed >-> addr_closed.
Coercion semiring_closedM : semiring_closed >-> mulr_closed.
Coercion subring_closedB : subring_closed >-> zmod_closed.
Coercion subring_closedM : subring_closed >-> smulr_closed.
Coercion subring_closed_semi : subring_closed >-> semiring_closed.
Coercion sdivr_closedM : sdivr_closed >-> smulr_closed.
Coercion sdivr_closed_div : sdivr_closed >-> divr_closed.
Coercion subalg_closedZ : subalg_closed >-> submod_closed.
Coercion subalg_closedBM : subalg_closed >-> subring_closed.
Coercion divring_closedBM : divring_closed >-> subring_closed.
Coercion divring_closed_div : divring_closed >-> sdivr_closed.
Coercion divalg_closedZ : divalg_closed >-> subalg_closed.
Coercion divalg_closedBdiv : divalg_closed >-> divring_closed.

Coercion opp_key : opp >-> pred_key.
Coercion add_key : add >-> pred_key.
Coercion mul_key : mul >-> pred_key.
Coercion zmod_opp : zmod >-> opp.
Canonical zmod_opp.
Coercion zmod_add : zmod >-> add.
Coercion semiring_add : semiring >-> add.
Coercion semiring_mul : semiring >-> mul.
Canonical semiring_mul.
Coercion smul_opp : smul >-> opp.
Coercion smul_mul : smul >-> mul.
Canonical smul_mul.
Coercion div_mul : div >-> mul.
Coercion submod_zmod : submod >-> zmod.
Coercion subring_zmod : subring >-> zmod.
Coercion subring_semi : subring >-> semiring.
Canonical subring_semi.
Coercion subring_smul : subring >-> smul.
Canonical subring_smul.
Coercion sdiv_smul : sdiv >-> smul.
Coercion sdiv_div : sdiv >-> div.
Canonical sdiv_div.
Coercion subalg_submod : subalg >-> submod.
Canonical subalg_submod.
Coercion subalg_ring : subalg >-> subring.
Coercion divring_ring : divring >-> subring.
Coercion divring_sdiv : divring >-> sdiv.
Canonical divring_sdiv.
Coercion divalg_alg : divalg >-> subalg.
Canonical divalg_alg.
Coercion divalg_ring : divalg >-> divring.

Notation opprPred := opp.
Notation addrPred := add.
Notation mulrPred := mul.
Notation zmodPred := zmod.
Notation semiringPred := semiring.
Notation smulrPred := smul.
Notation divrPred := div.
Notation submodPred := submod.
Notation subringPred := subring.
Notation sdivrPred := sdiv.
Notation subalgPred := subalg.
Notation divringPred := divring.
Notation divalgPred := divalg.

Definition OpprPred U S k kS NkS := Opp k (@opp_ext U S k kS NkS).
Definition AddrPred U S k kS DkS := Add k (@add_ext U S k kS DkS).
Definition MulrPred R S k kS MkS := Mul k (@mul_ext R S k kS MkS).
Definition ZmodPred U S k kS NkS := Zmod k (@opp_ext U S k kS NkS).
Definition SemiringPred R S k kS MkS := Semiring k (@mul_ext R S k kS MkS).
Definition SmulrPred R S k kS MkS := Smul k (@mul_ext R S k kS MkS).
Definition DivrPred R S k kS VkS := Div k (@inv_ext R S k kS VkS).
Definition SubmodPred R U S k kS ZkS := Submod k (@scale_ext R U S k kS ZkS).
Definition SubringPred R S k kS MkS := Subring k (@mul_ext R S k kS MkS).
Definition SdivrPred R S k kS VkS := Sdiv k (@inv_ext R S k kS VkS).
Definition SubalgPred (R : ringType) (A : lalgType R) S k kS ZkS :=
  Subalg k (@scale_ext R A S k kS ZkS).
Definition DivringPred R S k kS VkS := Divring k (@inv_ext R S k kS VkS).
Definition DivalgPred (R : ringType) (A : unitAlgType R) S k kS ZkS :=
  Divalg k (@scale_ext R A S k kS ZkS).

End Exports.

End Pred.
Import Pred.Exports.

Module DefaultPred.

Canonical Pred.Default.opp.
Canonical Pred.Default.add.
Canonical Pred.Default.mul.
Canonical Pred.Default.zmod.
Canonical Pred.Default.semiring.
Canonical Pred.Default.smul.
Canonical Pred.Default.div.
Canonical Pred.Default.submod.
Canonical Pred.Default.subring.
Canonical Pred.Default.sdiv.
Canonical Pred.Default.subalg.
Canonical Pred.Default.divring.
Canonical Pred.Default.divalg.

End DefaultPred.

Section ZmodulePred.

Variables (V : zmodType) (S : {pred V}).

Section Add.

Variables (addS : addrPred S) (kS : keyed_pred addS).

Lemma rpred0D : addr_closed kS.

Lemma rpred0 : 0 \in kS.

Lemma rpredD : {in kS &, u v, u + v \in kS}.

Lemma rpred_sum I r (P : pred I) F :
  ( i, P i F i \in kS) \sum_(i <- r | P i) F i \in kS.

Lemma rpredMn n : {in kS, u, u *+ n \in kS}.

End Add.

Section Opp.

Variables (oppS : opprPred S) (kS : keyed_pred oppS).

Lemma rpredNr : oppr_closed kS.

Lemma rpredN : {mono -%R: u / u \in kS}.

End Opp.

Section Sub.

Variables (subS : zmodPred S) (kS : keyed_pred subS).

Lemma rpredB : {in kS &, u v, u - v \in kS}.

Lemma rpredBC u v : u - v \in kS = (v - u \in kS).

Lemma rpredMNn n : {in kS, u, u *- n \in kS}.

Lemma rpredDr x y : x \in kS (y + x \in kS) = (y \in kS).

Lemma rpredDl x y : x \in kS (x + y \in kS) = (y \in kS).

Lemma rpredBr x y : x \in kS (y - x \in kS) = (y \in kS).

Lemma rpredBl x y : x \in kS (x - y \in kS) = (y \in kS).

End Sub.

End ZmodulePred.

Section RingPred.

Variables (R : ringType) (S : {pred R}).

Lemma rpredMsign (oppS : opprPred S) (kS : keyed_pred oppS) n x :
  ((-1) ^+ n × x \in kS) = (x \in kS).

Section Mul.

Variables (mulS : mulrPred S) (kS : keyed_pred mulS).

Lemma rpred1M : mulr_closed kS.

Lemma rpred1 : 1 \in kS.

Lemma rpredM : {in kS &, u v, u × v \in kS}.

Lemma rpred_prod I r (P : pred I) F :
  ( i, P i F i \in kS) \prod_(i <- r | P i) F i \in kS.

Lemma rpredX n : {in kS, u, u ^+ n \in kS}.

End Mul.

Lemma rpred_nat (rngS : semiringPred S) (kS : keyed_pred rngS) n : n%:R \in kS.

Lemma rpredN1 (mulS : smulrPred S) (kS : keyed_pred mulS) : -1 \in kS.

Lemma rpred_sign (mulS : smulrPred S) (kS : keyed_pred mulS) n :
  (-1) ^+ n \in kS.

End RingPred.

Section LmodPred.

Variables (R : ringType) (V : lmodType R) (S : {pred V}).

Lemma rpredZsign (oppS : opprPred S) (kS : keyed_pred oppS) n u :
  ((-1) ^+ n *: u \in kS) = (u \in kS).

Lemma rpredZnat (addS : addrPred S) (kS : keyed_pred addS) n :
  {in kS, u, n%:R *: u \in kS}.

Lemma rpredZ (linS : submodPred S) (kS : keyed_pred linS) : scaler_closed kS.

End LmodPred.

Section UnitRingPred.

Variable R : unitRingType.

Section Div.

Variables (S : {pred R}) (divS : divrPred S) (kS : keyed_pred divS).

Lemma rpredVr x : x \in kS x^-1 \in kS.

Lemma rpredV x : (x^-1 \in kS) = (x \in kS).

Lemma rpred_div : {in kS &, x y, x / y \in kS}.

Lemma rpredXN n : {in kS, x, x ^- n \in kS}.

Lemma rpredMl x y : x \in kS x \is a unit (x × y \in kS) = (y \in kS).

Lemma rpredMr x y : x \in kS x \is a unit (y × x \in kS) = (y \in kS).

Lemma rpred_divr x y : x \in kS x \is a unit (y / x \in kS) = (y \in kS).

Lemma rpred_divl x y : x \in kS x \is a unit (x / y \in kS) = (y \in kS).

End Div.

Fact unitr_sdivr_closed : @sdivr_closed R unit.

Canonical unit_opprPred := OpprPred unitr_sdivr_closed.
Canonical unit_mulrPred := MulrPred unitr_sdivr_closed.
Canonical unit_divrPred := DivrPred unitr_sdivr_closed.
Canonical unit_smulrPred := SmulrPred unitr_sdivr_closed.
Canonical unit_sdivrPred := SdivrPred unitr_sdivr_closed.

Implicit Type x : R.

Lemma unitrN x : (- x \is a unit) = (x \is a unit).

Lemma invrN x : (- x)^-1 = - x^-1.

Lemma divrNN x y : (- x) / (- y) = x / y.

Lemma divrN x y : x / (- y) = - (x / y).

Lemma invr_signM n x : ((-1) ^+ n × x)^-1 = (-1) ^+ n × x^-1.

Lemma divr_signM (b1 b2 : bool) x1 x2:
  ((-1) ^+ b1 × x1) / ((-1) ^+ b2 × x2) = (-1) ^+ (b1 (+) b2) × (x1 / x2).

End UnitRingPred.

Reification of the theory of rings with units, in named style
Section TermDef.

Variable R : Type.

Inductive term : Type :=
| Var of nat
| Const of R
| NatConst of nat
| Add of term & term
| Opp of term
| NatMul of term & nat
| Mul of term & term
| Inv of term
| Exp of term & nat.

Inductive formula : Type :=
| Bool of bool
| Equal of term & term
| Unit of term
| And of formula & formula
| Or of formula & formula
| Implies of formula & formula
| Not of formula
| Exists of nat & formula
| Forall of nat & formula.

End TermDef.

Bind Scope term_scope with term.
Bind Scope term_scope with formula.
Arguments Add {R} t1%T t2%T.
Arguments Opp {R} t1%T.
Arguments NatMul {R} t1%T n%N.
Arguments Mul {R} t1%T t2%T.
Arguments Inv {R} t1%T.
Arguments Exp {R} t1%T n%N.
Arguments Equal {R} t1%T t2%T.
Arguments Unit {R} t1%T.
Arguments And {R} f1%T f2%T.
Arguments Or {R} f1%T f2%T.
Arguments Implies {R} f1%T f2%T.
Arguments Not {R} f1%T.
Arguments Exists {R} i%N f1%T.
Arguments Forall {R} i%N f1%T.

Arguments Bool {R} b.
Arguments Const {R} x.

Notation True := (Bool true).
Notation False := (Bool false).


Section Substitution.

Variable R : Type.

Fixpoint tsubst (t : term R) (s : nat × term R) :=
  match t with
  | 'X_iif i == s.1 then s.2 else t
  | _%:T | _%:Rt
  | t1 + t2tsubst t1 s + tsubst t2 s
  | - t1- tsubst t1 s
  | t1 *+ ntsubst t1 s *+ n
  | t1 × t2tsubst t1 s × tsubst t2 s
  | t1^-1(tsubst t1 s)^-1
  | t1 ^+ ntsubst t1 s ^+ n
  end%T.

Fixpoint fsubst (f : formula R) (s : nat × term R) :=
  match f with
  | Bool _f
  | t1 == t2tsubst t1 s == tsubst t2 s
  | Unit t1Unit (tsubst t1 s)
  | f1 f2fsubst f1 s fsubst f2 s
  | f1 f2fsubst f1 s fsubst f2 s
  | f1 ==> f2fsubst f1 s ==> fsubst f2 s
  | ¬ f1¬ fsubst f1 s
  | (' 'X_i, f1) ⇒ ' 'X_i, if i == s.1 then f1 else fsubst f1 s
  | (' 'X_i, f1) ⇒ ' 'X_i, if i == s.1 then f1 else fsubst f1 s
  end%T.

End Substitution.

Section EvalTerm.

Variable R : unitRingType.

Evaluation of a reified term into R a ring with units
Fixpoint eval (e : seq R) (t : term R) {struct t} : R :=
  match t with
  | ('X_i)%Te`_i
  | (x%:T)%Tx
  | (n%:R)%Tn%:R
  | (t1 + t2)%Teval e t1 + eval e t2
  | (- t1)%T- eval e t1
  | (t1 *+ n)%Teval e t1 *+ n
  | (t1 × t2)%Teval e t1 × eval e t2
  | t1^-1%T(eval e t1)^-1
  | (t1 ^+ n)%Teval e t1 ^+ n
  end.

Definition same_env (e e' : seq R) := nth 0 e =1 nth 0 e'.

Lemma eq_eval e e' t : same_env e e' eval e t = eval e' t.

Lemma eval_tsubst e t s :
  eval e (tsubst t s) = eval (set_nth 0 e s.1 (eval e s.2)) t.

Evaluation of a reified formula
Fixpoint holds (e : seq R) (f : formula R) {struct f} : Prop :=
  match f with
  | Bool bb
  | (t1 == t2)%Teval e t1 = eval e t2
  | Unit t1eval e t1 \in unit
  | (f1 f2)%Tholds e f1 holds e f2
  | (f1 f2)%Tholds e f1 holds e f2
  | (f1 ==> f2)%Tholds e f1 holds e f2
  | (¬ f1)%T¬ holds e f1
  | (' 'X_i, f1)%T x, holds (set_nth 0 e i x) f1
  | (' 'X_i, f1)%T x, holds (set_nth 0 e i x) f1
  end.

Lemma same_env_sym e e' : same_env e e' same_env e' e.

Extensionality of formula evaluation
Evaluation and substitution by a constant
Lemma holds_fsubst e f i v :
  holds e (fsubst f (i, v%:T)%T) holds (set_nth 0 e i v) f.

Boolean test selecting terms in the language of rings
Fixpoint rterm (t : term R) :=
  match t with
  | _^-1false
  | t1 + t2 | t1 × t2rterm t1 && rterm t2
  | - t1 | t1 *+ _ | t1 ^+ _rterm t1
  | _true
  end%T.

Boolean test selecting formulas in the theory of rings
Fixpoint rformula (f : formula R) :=
  match f with
  | Bool _true
  | t1 == t2rterm t1 && rterm t2
  | Unit t1false
  | f1 f2 | f1 f2 | f1 ==> f2rformula f1 && rformula f2
  | ¬ f1 | (' 'X__, f1) | (' 'X__, f1) ⇒ rformula f1
  end%T.

Upper bound of the names used in a term
Fixpoint ub_var (t : term R) :=
  match t with
  | 'X_ii.+1
  | t1 + t2 | t1 × t2maxn (ub_var t1) (ub_var t2)
  | - t1 | t1 *+ _ | t1 ^+ _ | t1^-1ub_var t1
  | _ ⇒ 0%N
  end%T.

Replaces inverses in the term t by fresh variables, accumulating the substitution.
Fixpoint to_rterm (t : term R) (r : seq (term R)) (n : nat) {struct t} :=
  match t with
  | t1^-1
    let: (t1', r1) := to_rterm t1 r n in
      ('X_(n + size r1), rcons r1 t1')
  | t1 + t2
    let: (t1', r1) := to_rterm t1 r n in
    let: (t2', r2) := to_rterm t2 r1 n in
      (t1' + t2', r2)
  | - t1
   let: (t1', r1) := to_rterm t1 r n in
     (- t1', r1)
  | t1 *+ m
   let: (t1', r1) := to_rterm t1 r n in
     (t1' *+ m, r1)
  | t1 × t2
    let: (t1', r1) := to_rterm t1 r n in
    let: (t2', r2) := to_rterm t2 r1 n in
      (Mul t1' t2', r2)
  | t1 ^+ m
       let: (t1', r1) := to_rterm t1 r n in
     (t1' ^+ m, r1)
  | _(t, r)
  end%T.

Lemma to_rterm_id t r n : rterm t to_rterm t r n = (t, r).

A ring formula stating that t1 is equal to 0 in the ring theory. Also applies to non commutative rings.
Definition eq0_rform t1 :=
  let m := ub_var t1 in
  let: (t1', r1) := to_rterm t1 [::] m in
  let fix loop r i := match r with
  | [::]t1' == 0
  | t :: r'
    let f := 'X_i × t == 1 t × 'X_i == 1 in
     ' 'X_i, (f 'X_i == t ¬ (' 'X_i, f)) ==> loop r' i.+1
  end%T
  in loop r1 m.

Transformation of a formula in the theory of rings with units into an equivalent formula in the sub-theory of rings.
Fixpoint to_rform f :=
  match f with
  | Bool bf
  | t1 == t2eq0_rform (t1 - t2)
  | Unit t1eq0_rform (t1 × t1^-1 - 1)
  | f1 f2to_rform f1 to_rform f2
  | f1 f2to_rform f1 to_rform f2
  | f1 ==> f2to_rform f1 ==> to_rform f2
  | ¬ f1¬ to_rform f1
  | (' 'X_i, f1) ⇒ ' 'X_i, to_rform f1
  | (' 'X_i, f1) ⇒ ' 'X_i, to_rform f1
  end%T.

The transformation gives a ring formula.
Correctness of the transformation.
Boolean test selecting formulas which describe a constructible set, i.e. formulas without quantifiers.
The quantifier elimination check.
Fixpoint qf_form (f : formula R) :=
  match f with
  | Bool _ | _ == _ | Unit _true
  | f1 f2 | f1 f2 | f1 ==> f2qf_form f1 && qf_form f2
  | ¬ f1qf_form f1
  | _false
  end%T.

Boolean holds predicate for quantifier free formulas
Definition qf_eval e := fix loop (f : formula R) : bool :=
  match f with
  | Bool bb
  | t1 == t2 ⇒ (eval e t1 == eval e t2)%bool
  | Unit t1eval e t1 \in unit
  | f1 f2loop f1 && loop f2
  | f1 f2loop f1 || loop f2
  | f1 ==> f2 ⇒ (loop f1 ==> loop f2)%bool
  | ¬ f1~~ loop f1
  |_false
  end%T.

qf_eval is equivalent to holds
Lemma qf_evalP e f : qf_form f reflect (holds e f) (qf_eval e f).

Implicit Type bc : seq (term R) × seq (term R).

Quantifier-free formula are normalized into DNF. A DNF is represented by the type seq (seq (term R) * seq (term R)), where we separate positive and negative literals
DNF preserving conjunction
Definition and_dnf bcs1 bcs2 :=
  \big[cat/nil]_(bc1 <- bcs1)
     map (fun bc2(bc1.1 ++ bc2.1, bc1.2 ++ bc2.2)) bcs2.

Computes a DNF from a qf ring formula
Fixpoint qf_to_dnf (f : formula R) (neg : bool) {struct f} :=
  match f with
  | Bool bif b (+) neg then [:: ([::], [::])] else [::]
  | t1 == t2[:: if neg then ([::], [:: t1 - t2]) else ([:: t1 - t2], [::])]
  | f1 f2(if neg then cat else and_dnf) [rec f1, neg] [rec f2, neg]
  | f1 f2(if neg then and_dnf else cat) [rec f1, neg] [rec f2, neg]
  | f1 ==> f2(if neg then and_dnf else cat) [rec f1, ~~ neg] [rec f2, neg]
  | ¬ f1[rec f1, ~~ neg]
  | _if neg then [:: ([::], [::])] else [::]
  end%T where "[ 'rec' f , neg ]" := (qf_to_dnf f neg).

Conversely, transforms a DNF into a formula
Definition dnf_to_form :=
  let pos_lit t := And (t == 0) in let neg_lit t := And (t != 0) in
  let cls bc := Or (foldr pos_lit True bc.1 foldr neg_lit True bc.2) in
  foldr cls False.

Catenation of dnf is the Or of formulas
and_dnf is the And of formulas
Lemma and_dnfP e bcs1 bcs2 :
  qf_eval e (dnf_to_form (and_dnf bcs1 bcs2))
   = qf_eval e (dnf_to_form bcs1 dnf_to_form bcs2).

Lemma qf_to_dnfP e :
  let qev f b := qf_eval e (dnf_to_form (qf_to_dnf f b)) in
   f, qf_form f && rformula f qev f false = qf_eval e f.

Lemma dnf_to_form_qf bcs : qf_form (dnf_to_form bcs).

Definition dnf_rterm cl := all rterm cl.1 && all rterm cl.2.

Lemma qf_to_dnf_rterm f b : rformula f all dnf_rterm (qf_to_dnf f b).

Lemma dnf_to_rform bcs : rformula (dnf_to_form bcs) = all dnf_rterm bcs.

Section If.

Variables (pred_f then_f else_f : formula R).

Definition If := (pred_f then_f ¬ pred_f else_f)%T.

Lemma If_form_qf :
  qf_form pred_f qf_form then_f qf_form else_f qf_form If.

Lemma If_form_rf :
  rformula pred_f rformula then_f rformula else_f rformula If.

Lemma eval_If e :
  let ev := qf_eval e in ev If = (if ev pred_f then ev then_f else ev else_f).

End If.

Section Pick.

Variables (I : finType) (pred_f then_f : I formula R) (else_f : formula R).

Definition Pick :=
  \big[Or/False]_(p : {ffun pred I})
    ((\big[And/True]_i (if p i then pred_f i else ¬ pred_f i))
     (if pick p is Some i then then_f i else else_f))%T.

Lemma Pick_form_qf :
   ( i, qf_form (pred_f i))
   ( i, qf_form (then_f i))
    qf_form else_f
  qf_form Pick.

Lemma eval_Pick e (qev := qf_eval e) :
  let P i := qev (pred_f i) in
  qev Pick = (if pick P is Some i then qev (then_f i) else qev else_f).

End Pick.

Section MultiQuant.

Variable f : formula R.
Implicit Types (I : seq nat) (e : seq R).

Lemma foldExistsP I e :
  (exists2 e', {in [predC I], same_env e e'} & holds e' f)
     holds e (foldr Exists f I).

Lemma foldForallP I e :
  ( e', {in [predC I], same_env e e'} holds e' f)
     holds e (foldr Forall f I).

End MultiQuant.

End EvalTerm.


Module IntegralDomain.

Definition axiom (R : ringType) :=
   x y : R, x × y = 0 (x == 0) || (y == 0).

Section ClassDef.

Record class_of (R : Type) : Type :=
  Class {base : ComUnitRing.class_of R; mixin : axiom (Ring.Pack base)}.

Structure type := Pack {sort; _ : class_of sort}.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) :=
  fun bT b & phant_id (ComUnitRing.class bT) b
  fun m & phant_id m0 mPack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition comUnitRingType := @ComUnitRing.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> ComUnitRing.class_of.
Arguments mixin [R] c [x y].
Coercion mixin : class_of >-> axiom.
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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical comUnitRingType.
Notation idomainType := type.
Notation IdomainType T m := (@pack T _ m _ _ id _ id).
Notation "[ 'idomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'idomainType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'idomainType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'idomainType' 'of' T ]") : form_scope.
End Exports.

End IntegralDomain.
Import IntegralDomain.Exports.

Section IntegralDomainTheory.

Variable R : idomainType.
Implicit Types x y : R.

Lemma mulf_eq0 x y : (x × y == 0) = (x == 0) || (y == 0).

Lemma prodf_eq0 (I : finType) (P : pred I) (F : I R) :
  reflect (exists2 i, P i & (F i == 0)) (\prod_(i | P i) F i == 0).

Lemma prodf_seq_eq0 I r (P : pred I) (F : I R) :
  (\prod_(i <- r | P i) F i == 0) = has (fun iP i && (F i == 0)) r.

Lemma mulf_neq0 x y : x != 0 y != 0 x × y != 0.

Lemma prodf_neq0 (I : finType) (P : pred I) (F : I R) :
  reflect ( i, P i (F i != 0)) (\prod_(i | P i) F i != 0).

Lemma prodf_seq_neq0 I r (P : pred I) (F : I R) :
  (\prod_(i <- r | P i) F i != 0) = all (fun iP i ==> (F i != 0)) r.

Lemma expf_eq0 x n : (x ^+ n == 0) = (n > 0) && (x == 0).

Lemma sqrf_eq0 x : (x ^+ 2 == 0) = (x == 0).

Lemma expf_neq0 x m : x != 0 x ^+ m != 0.

Lemma natf_neq0 n : (n%:R != 0 :> R) = [char R]^'.-nat n.

Lemma natf0_char n : n > 0 n%:R == 0 :> R p, p \in [char R].

Lemma charf'_nat n : [char R]^'.-nat n = (n%:R != 0 :> R).

Lemma charf0P : [char R] =i pred0 ( n, (n%:R == 0 :> R) = (n == 0)%N).

Lemma eqf_sqr x y : (x ^+ 2 == y ^+ 2) = (x == y) || (x == - y).

Lemma mulfI x : x != 0 injective ( *%R x).

Lemma mulIf x : x != 0 injective ( *%R^~ x).

Lemma divfI x : x != 0 injective (fun yx / y).

Lemma divIf y : y != 0 injective (fun xx / y).

Lemma sqrf_eq1 x : (x ^+ 2 == 1) = (x == 1) || (x == -1).

Lemma expfS_eq1 x n :
  (x ^+ n.+1 == 1) = (x == 1) || (\sum_(i < n.+1) x ^+ i == 0).

Lemma lregP x : reflect (lreg x) (x != 0).

Lemma rregP x : reflect (rreg x) (x != 0).

Canonical regular_idomainType := [idomainType of R^o].

End IntegralDomainTheory.

Arguments lregP {R x}.
Arguments rregP {R x}.

Module Field.

Definition mixin_of (R : unitRingType) := x : R, x != 0 x \in unit.

Lemma IdomainMixin R : mixin_of R IntegralDomain.axiom R.

Section Mixins.

Definition axiom (R : ringType) inv := x : R, x != 0 inv x × x = 1.

Variables (R : comRingType) (inv : R R).
Hypotheses (mulVf : axiom inv) (inv0 : inv 0 = 0).

Fact intro_unit (x y : R) : y × x = 1 x != 0.

Fact inv_out : {in predC (predC1 0), inv =1 id}.

Definition UnitMixin := ComUnitRing.Mixin mulVf intro_unit inv_out.

Definition UnitRingType := [comUnitRingType of UnitRingType R UnitMixin].

Definition IdomainType :=
  IdomainType UnitRingType (@IdomainMixin UnitRingType (fun id)).

Lemma Mixin : mixin_of IdomainType.

End Mixins.

Section ClassDef.

Record class_of (F : Type) : Type := Class {
  base : IntegralDomain.class_of F;
  mixin : mixin_of (UnitRing.Pack base)
}.

Structure type := Pack {sort; _ : class_of sort}.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) :=
  fun bT b & phant_id (IntegralDomain.class bT) b
  fun m & phant_id m0 mPack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition comUnitRingType := @ComUnitRing.Pack cT class.
Definition idomainType := @IntegralDomain.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> IntegralDomain.class_of.
Arguments mixin [F] c [x].
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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical idomainType.
Notation fieldType := type.
Notation FieldType T m := (@pack T _ m _ _ id _ id).
Arguments Mixin {R inv} mulVf inv0 [x] nz_x.
Notation FieldUnitMixin := UnitMixin.
Notation FieldIdomainMixin := IdomainMixin.
Notation FieldMixin := Mixin.
Notation "[ 'fieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'fieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'fieldType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'fieldType' 'of' T ]") : form_scope.
End Exports.

End Field.
Import Field.Exports.

Section FieldTheory.

Variable F : fieldType.
Implicit Types x y : F.

Lemma fieldP : Field.mixin_of F.

Lemma unitfE x : (x \in unit) = (x != 0).

Lemma mulVf x : x != 0 x^-1 × x = 1.
Lemma divff x : x != 0 x / x = 1.
Definition mulfV := divff.
Lemma mulKf x : x != 0 cancel ( *%R x) ( *%R x^-1).
Lemma mulVKf x : x != 0 cancel ( *%R x^-1) ( *%R x).
Lemma mulfK x : x != 0 cancel ( *%R^~ x) ( *%R^~ x^-1).
Lemma mulfVK x : x != 0 cancel ( *%R^~ x^-1) ( *%R^~ x).
Definition divfK := mulfVK.

Lemma invfM : {morph @inv F : x y / x × y}.

Lemma invf_div x y : (x / y)^-1 = y / x.

Lemma divKf x : x != 0 involutive (fun yx / y).

Lemma expfB_cond m n x : (x == 0) + n m x ^+ (m - n) = x ^+ m / x ^+ n.

Lemma expfB m n x : n < m x ^+ (m - n) = x ^+ m / x ^+ n.

Lemma prodfV I r (P : pred I) (E : I F) :
  \prod_(i <- r | P i) (E i)^-1 = (\prod_(i <- r | P i) E i)^-1.

Lemma prodf_div I r (P : pred I) (E D : I F) :
  \prod_(i <- r | P i) (E i / D i) =
     \prod_(i <- r | P i) E i / \prod_(i <- r | P i) D i.

Lemma telescope_prodf n m (f : nat F) :
    ( k, n < k < m f k != 0) n < m
  \prod_(n k < m) (f k.+1 / f k) = f m / f n.

Lemma telescope_prodf_eq n m (f u : nat F) :
    ( k, n < k < m f k != 0) n < m
    ( k, n k < m u k = f k.+1 / f k)
  \prod_(n k < m) u k = f m / f n.

Lemma addf_div x1 y1 x2 y2 :
  y1 != 0 y2 != 0 x1 / y1 + x2 / y2 = (x1 × y2 + x2 × y1) / (y1 × y2).

Lemma mulf_div x1 y1 x2 y2 : (x1 / y1) × (x2 / y2) = (x1 × x2) / (y1 × y2).

Lemma eqr_div x y z t : y != 0 t != 0 (x / y == z / t) = (x × t == z × y).

Lemma eqr_sum_div I r P (f : I F) c a : c != 0
  \big[+%R/0]_(x <- r | P x) (f x / c) == a
  = (\big[+%R/0]_(x <- r | P x) f x == a × c).

Lemma char0_natf_div :
  [char F] =i pred0 m d, d %| m (m %/ d)%:R = m%:R / d%:R :> F.

Section FieldMorphismInj.

Variables (R : ringType) (f : {rmorphism F R}).

Lemma fmorph_eq0 x : (f x == 0) = (x == 0).

Lemma fmorph_inj : injective f.

Lemma fmorph_eq : {mono f : x y / x == y}.

Lemma fmorph_eq1 x : (f x == 1) = (x == 1).

Lemma fmorph_char : [char R] =i [char F].

End FieldMorphismInj.

Section FieldMorphismInv.

Variables (R : unitRingType) (f : {rmorphism F R}).

Lemma fmorph_unit x : (f x \in unit) = (x != 0).

Lemma fmorphV : {morph f: x / x^-1}.

Lemma fmorph_div : {morph f : x y / x / y}.

End FieldMorphismInv.

Canonical regular_fieldType := [fieldType of F^o].

Section ModuleTheory.

Variable V : lmodType F.
Implicit Types (a : F) (v : V).

Lemma scalerK a : a != 0 cancel ( *:%R a : V V) ( *:%R a^-1).

Lemma scalerKV a : a != 0 cancel ( *:%R a^-1 : V V) ( *:%R a).

Lemma scalerI a : a != 0 injective ( *:%R a : V V).

Lemma scaler_eq0 a v : (a *: v == 0) = (a == 0) || (v == 0).

Lemma rpredZeq S (modS : submodPred S) (kS : keyed_pred modS) a v :
  (a *: v \in kS) = (a == 0) || (v \in kS).

End ModuleTheory.

Lemma char_lalg (A : lalgType F) : [char A] =i [char F].

Section Predicates.

Context (S : {pred F}) (divS : @divrPred F S) (kS : keyed_pred divS).

Lemma fpredMl x y : x \in kS x != 0 (x × y \in kS) = (y \in kS).

Lemma fpredMr x y : x \in kS x != 0 (y × x \in kS) = (y \in kS).

Lemma fpred_divl x y : x \in kS x != 0 (x / y \in kS) = (y \in kS).

Lemma fpred_divr x y : x \in kS x != 0 (y / x \in kS) = (y \in kS).

End Predicates.

End FieldTheory.

Arguments fmorph_inj {F R} f [x1 x2].
Arguments telescope_prodf_eq {F n m} f u.

Module DecidableField.

Definition axiom (R : unitRingType) (s : seq R pred (formula R)) :=
   e f, reflect (holds e f) (s e f).

Record mixin_of (R : unitRingType) : Type :=
  Mixin { sat : seq R pred (formula R); satP : axiom sat}.

Section ClassDef.

Record class_of (F : Type) : Type :=
  Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base)}.

Structure type := Pack {sort; _ : class_of sort}.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) :=
  fun bT b & phant_id (Field.class bT) b
  fun m & phant_id m0 mPack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition comUnitRingType := @ComUnitRing.Pack cT class.
Definition idomainType := @IntegralDomain.Pack cT class.
Definition fieldType := @Field.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Field.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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical idomainType.
Coercion fieldType : type >-> Field.type.
Canonical fieldType.
Notation decFieldType := type.
Notation DecFieldType T m := (@pack T _ m _ _ id _ id).
Notation DecFieldMixin := Mixin.
Notation "[ 'decFieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'decFieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'decFieldType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'decFieldType' 'of' T ]") : form_scope.
End Exports.

End DecidableField.
Import DecidableField.Exports.

Section DecidableFieldTheory.

Variable F : decFieldType.

Definition sat := DecidableField.sat (DecidableField.class F).

Lemma satP : DecidableField.axiom sat.

Fact sol_subproof n f :
  reflect ( s, (size s == n) && sat s f)
          (sat [::] (foldr Exists f (iota 0 n))).

Definition sol n f :=
  if sol_subproof n f is ReflectT sP then xchoose sP else nseq n 0.

Lemma size_sol n f : size (sol n f) = n.

Lemma solP n f : reflect (exists2 s, size s = n & holds s f) (sat (sol n f) f).

Lemma eq_sat f1 f2 :
  ( e, holds e f1 holds e f2) sat^~ f1 =1 sat^~ f2.

Lemma eq_sol f1 f2 :
  ( e, holds e f1 holds e f2) sol^~ f1 =1 sol^~ f2.

End DecidableFieldTheory.

Arguments satP {F e f}.
Arguments solP {F n f}.

Section QE_Mixin.

Variable F : Field.type.
Implicit Type f : formula F.

Variable proj : nat seq (term F) × seq (term F) formula F.
proj is the elimination of a single existential quantifier
The elimination projector is well_formed.
Definition wf_QE_proj :=
   i bc (bc_i := proj i bc),
  dnf_rterm bc qf_form bc_i && rformula bc_i.

The elimination projector is valid
Axiom == all non-constant monic polynomials have a root
Definition axiom (R : ringType) :=
   n (P : nat R), n > 0
    x : R, x ^+ n = \sum_(i < n) P i × (x ^+ i).

Section ClassDef.

Record class_of (F : Type) : Type :=
  Class {base : DecidableField.class_of F; mixin : axiom (Ring.Pack base)}.

Structure type := Pack {sort; _ : class_of sort}.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) :=
  fun bT b & phant_id (DecidableField.class bT) b
  fun m & phant_id m0 mPack (@Class T b m).

There should eventually be a constructor from polynomial resolution that builds the DecidableField mixin using QE.

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition comUnitRingType := @ComUnitRing.Pack cT class.
Definition idomainType := @IntegralDomain.Pack cT class.
Definition fieldType := @Field.Pack cT class.
Definition decFieldType := @DecidableField.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> DecidableField.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 zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical idomainType.
Coercion fieldType : type >-> Field.type.
Canonical fieldType.
Coercion decFieldType : type >-> DecidableField.type.
Canonical decFieldType.
Notation closedFieldType := type.
Notation ClosedFieldType T m := (@pack T _ m _ _ id _ id).
Notation "[ 'closedFieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'closedFieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'closedFieldType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'closedFieldType' 'of' T ]") : form_scope.
End Exports.

End ClosedField.
Import ClosedField.Exports.

Section ClosedFieldTheory.

Variable F : closedFieldType.

Lemma solve_monicpoly : ClosedField.axiom F.

Lemma imaginary_exists : {i : F | i ^+ 2 = -1}.

End ClosedFieldTheory.

Module SubType.

Section Zmodule.

Variables (V : zmodType) (S : {pred V}).
Variables (subS : zmodPred S) (kS : keyed_pred subS).
Variable U : subType [in kS].

Let inU v Sv : U := Sub v Sv.
Let zeroU := inU (rpred0 kS).

Let oppU (u : U) := inU (rpredNr (valP u)).
Let addU (u1 u2 : U) := inU (rpredD (valP u1) (valP u2)).

Fact addA : associative addU.
Fact addC : commutative addU.
Fact add0 : left_id zeroU addU.
Fact addN : left_inverse zeroU oppU addU.

Definition zmodMixin of phant U := ZmodMixin addA addC add0 addN.

End Zmodule.

Section Ring.

Variables (R : ringType) (S : {pred R}).
Variables (ringS : subringPred S) (kS : keyed_pred ringS).

Definition cast_zmodType (V : zmodType) T (VeqT : V = T :> Type) :=
  let cast mV := let: erefl in _ = T := VeqT return Zmodule.class_of T in mV in
  Zmodule.Pack (cast (Zmodule.class V)).

Variable (T : subType [in kS]) (V : zmodType) (VeqT: V = T :> Type).

Let inT x Sx : T := Sub x Sx.
Let oneT := inT (rpred1 kS).
Let mulT (u1 u2 : T) := inT (rpredM (valP u1) (valP u2)).
Let T' := cast_zmodType VeqT.

Hypothesis valM : {morph (val : T' R) : x y / x - y}.

Let val0 : val (0 : T') = 0.
Let valD : {morph (val : T' R): x y / x + y}.

Fact mulA : @associative T' mulT.
Fact mul1l : left_id oneT mulT.
Fact mul1r : right_id oneT mulT.
Fact mulDl : @left_distributive T' T' mulT +%R.
Fact mulDr : @right_distributive T' T' mulT +%R.
Fact nz1 : oneT != 0 :> T'.

Definition ringMixin := RingMixin mulA mul1l mul1r mulDl mulDr nz1.

End Ring.

Section Lmodule.

Variables (R : ringType) (V : lmodType R) (S : {pred V}).
Variables (linS : submodPred S) (kS : keyed_pred linS).
Variables (W : subType [in kS]) (Z : zmodType) (ZeqW : Z = W :> Type).

Let scaleW a (w : W) := (Sub _ : _ W) (rpredZ a (valP w)).
Let W' := cast_zmodType ZeqW.

Hypothesis valD : {morph (val : W' V) : x y / x + y}.

Fact scaleA a b (w : W') : scaleW a (scaleW b w) = scaleW (a × b) w.
Fact scale1 : left_id 1 scaleW.
Fact scaleDr : @right_distributive R W' scaleW +%R.
Fact scaleDl w : {morph (scaleW^~ w : R W') : a b / a + b}.

Definition lmodMixin := LmodMixin scaleA scale1 scaleDr scaleDl.

End Lmodule.

Lemma lalgMixin (R : ringType) (A : lalgType R) (B : lmodType R) (f : B A) :
     phant B injective f scalable f
    mulB, {morph f : x y / mulB x y >-> x × y} Lalgebra.axiom mulB.

Lemma comRingMixin (R : comRingType) (T : ringType) (f : T R) :
  phant T injective f {morph f : x y / x × y} commutative (@mul T).

Lemma algMixin (R : comRingType) (A : algType R) (B : lalgType R) (f : B A) :
    phant B injective f {morph f : x y / x × y} scalable f
  @Algebra.axiom R B.

Section UnitRing.

Definition cast_ringType (Q : ringType) T (QeqT : Q = T :> Type) :=
  let cast rQ := let: erefl in _ = T := QeqT return Ring.class_of T in rQ in
  Ring.Pack (cast (Ring.class Q)).

Variables (R : unitRingType) (S : {pred R}).
Variables (ringS : divringPred S) (kS : keyed_pred ringS).

Variables (T : subType [in kS]) (Q : ringType) (QeqT : Q = T :> Type).

Let inT x Sx : T := Sub x Sx.
Let invT (u : T) := inT (rpredVr (valP u)).
Let unitT := [qualify a u : T | val u \is a unit].
Let T' := cast_ringType QeqT.

Hypothesis val1 : val (1 : T') = 1.
Hypothesis valM : {morph (val : T' R) : x y / x × y}.

Fact mulVr :
  {in (unitT : {pred T'}), left_inverse (1 : T') invT (@mul T')}.

Fact mulrV : {in unitT, right_inverse (1 : T') invT (@mul T')}.

Fact unitP (u v : T') : v × u = 1 u × v = 1 u \in unitT.

Fact unit_id : {in [predC unitT], invT =1 id}.

Definition unitRingMixin := UnitRingMixin mulVr mulrV unitP unit_id.

End UnitRing.

Lemma idomainMixin (R : idomainType) (T : ringType) (f : T R) :
    phant T injective f f 0 = 0 {morph f : u v / u × v}
  @IntegralDomain.axiom T.

Lemma fieldMixin (F : fieldType) (K : unitRingType) (f : K F) :
    phant K injective f f 0 = 0 {mono f : u / u \in unit}
  @Field.mixin_of K.

Module Exports.

Notation "[ 'zmodMixin' 'of' U 'by' <: ]" := (zmodMixin (Phant U))
  (at level 0, format "[ 'zmodMixin' 'of' U 'by' <: ]") : form_scope.
Notation "[ 'ringMixin' 'of' R 'by' <: ]" :=
  (@ringMixin _ _ _ _ _ _ (@erefl Type R%type) (rrefl _))
  (at level 0, format "[ 'ringMixin' 'of' R 'by' <: ]") : form_scope.
Notation "[ 'lmodMixin' 'of' U 'by' <: ]" :=
  (@lmodMixin _ _ _ _ _ _ _ (@erefl Type U%type) (rrefl _))
  (at level 0, format "[ 'lmodMixin' 'of' U 'by' <: ]") : form_scope.
Notation "[ 'lalgMixin' 'of' A 'by' <: ]" :=
  ((lalgMixin (Phant A) val_inj (rrefl _)) *%R (rrefl _))
  (at level 0, format "[ 'lalgMixin' 'of' A 'by' <: ]") : form_scope.
Notation "[ 'comRingMixin' 'of' R 'by' <: ]" :=
  (comRingMixin (Phant R) val_inj (rrefl _))
  (at level 0, format "[ 'comRingMixin' 'of' R 'by' <: ]") : form_scope.
Notation "[ 'algMixin' 'of' A 'by' <: ]" :=
  (algMixin (Phant A) val_inj (rrefl _) (rrefl _))
  (at level 0, format "[ 'algMixin' 'of' A 'by' <: ]") : form_scope.
Notation "[ 'unitRingMixin' 'of' R 'by' <: ]" :=
  (@unitRingMixin _ _ _ _ _ _ (@erefl Type R%type) (erefl _) (rrefl _))
  (at level 0, format "[ 'unitRingMixin' 'of' R 'by' <: ]") : form_scope.
Notation "[ 'idomainMixin' 'of' R 'by' <: ]" :=
  (idomainMixin (Phant R) val_inj (erefl _) (rrefl _))
  (at level 0, format "[ 'idomainMixin' 'of' R 'by' <: ]") : form_scope.
Notation "[ 'fieldMixin' 'of' F 'by' <: ]" :=
  (fieldMixin (Phant F) val_inj (erefl _) (frefl _))
  (at level 0, format "[ 'fieldMixin' 'of' F 'by' <: ]") : form_scope.

End Exports.

End SubType.

Module Theory.

Definition addrA := addrA.
Definition addrC := addrC.
Definition add0r := add0r.
Definition addNr := addNr.
Definition addr0 := addr0.
Definition addrN := addrN.
Definition subrr := subrr.
Definition addrCA := addrCA.
Definition addrAC := addrAC.
Definition addrACA := addrACA.
Definition addKr := addKr.
Definition addNKr := addNKr.
Definition addrK := addrK.
Definition addrNK := addrNK.
Definition subrK := subrK.
Definition subKr := subKr.
Definition addrI := @addrI.
Definition addIr := @addIr.
Definition subrI := @subrI.
Definition subIr := @subIr.
Arguments addrI {V} y [x1 x2].
Arguments addIr {V} x [x1 x2].
Arguments subrI {V} y [x1 x2].
Arguments subIr {V} x [x1 x2].
Definition opprK := @opprK.
Arguments opprK {V}.
Definition oppr_inj := @oppr_inj.
Arguments oppr_inj {V} [x1 x2].
Definition oppr0 := oppr0.
Definition oppr_eq0 := oppr_eq0.
Definition opprD := opprD.
Definition opprB := opprB.
Definition addrKA := addrKA.
Definition subrKA := subrKA.
Definition subr0 := subr0.
Definition sub0r := sub0r.
Definition subr_eq := subr_eq.
Definition addr0_eq := addr0_eq.
Definition subr0_eq := subr0_eq.
Definition subr_eq0 := subr_eq0.
Definition addr_eq0 := addr_eq0.
Definition eqr_opp := eqr_opp.
Definition eqr_oppLR := eqr_oppLR.
Definition sumrN := sumrN.
Definition sumrB := sumrB.
Definition sumrMnl := sumrMnl.
Definition sumrMnr := sumrMnr.
Definition sumr_const := sumr_const.
Definition sumr_const_nat := sumr_const_nat.
Definition telescope_sumr := telescope_sumr.
Definition telescope_sumr_eq := @telescope_sumr_eq.
Arguments telescope_sumr_eq {V n m} f u.
Definition mulr0n := mulr0n.
Definition mulr1n := mulr1n.
Definition mulr2n := mulr2n.
Definition mulrS := mulrS.
Definition mulrSr := mulrSr.
Definition mulrb := mulrb.
Definition mul0rn := mul0rn.
Definition mulNrn := mulNrn.
Definition mulrnDl := mulrnDl.
Definition mulrnDr := mulrnDr.
Definition mulrnBl := mulrnBl.
Definition mulrnBr := mulrnBr.
Definition mulrnA := mulrnA.
Definition mulrnAC := mulrnAC.
Definition iter_addr := iter_addr.
Definition iter_addr_0 := iter_addr_0.
Definition mulrA := mulrA.
Definition mul1r := mul1r.
Definition mulr1 := mulr1.
Definition mulrDl := mulrDl.
Definition mulrDr := mulrDr.
Definition oner_neq0 := oner_neq0.
Definition oner_eq0 := oner_eq0.
Definition mul0r := mul0r.
Definition mulr0 := mulr0.
Definition mulrN := mulrN.
Definition mulNr := mulNr.
Definition mulrNN := mulrNN.
Definition mulN1r := mulN1r.
Definition mulrN1 := mulrN1.
Definition mulr_suml := mulr_suml.
Definition mulr_sumr := mulr_sumr.
Definition mulrBl := mulrBl.
Definition mulrBr := mulrBr.
Definition mulrnAl := mulrnAl.
Definition mulrnAr := mulrnAr.
Definition mulr_natl := mulr_natl.
Definition mulr_natr := mulr_natr.
Definition natrD := natrD.
Definition nat1r := nat1r.
Definition natr1 := natr1.
Definition natrB := natrB.
Definition natr_sum := natr_sum.
Definition natrM := natrM.
Definition natrX := natrX.
Definition expr0 := expr0.
Definition exprS := exprS.
Definition expr1 := expr1.
Definition expr2 := expr2.
Definition expr0n := expr0n.
Definition expr1n := expr1n.
Definition exprD := exprD.
Definition exprSr := exprSr.
Definition expr_sum := expr_sum.
Definition commr_sym := commr_sym.
Definition commr_refl := commr_refl.
Definition commr0 := commr0.
Definition commr1 := commr1.
Definition commrN := commrN.
Definition commrN1 := commrN1.
Definition commrD := commrD.
Definition commrB := commrB.
Definition commr_sum := commr_sum.
Definition commr_prod := commr_prod.
Definition commrMn := commrMn.
Definition commrM := commrM.
Definition commr_nat := commr_nat.
Definition commrX := commrX.
Definition exprMn_comm := exprMn_comm.
Definition commr_sign := commr_sign.
Definition exprMn_n := exprMn_n.
Definition exprM := exprM.
Definition exprAC := exprAC.
Definition expr_mod := expr_mod.
Definition expr_dvd := expr_dvd.
Definition signr_odd := signr_odd.
Definition signr_eq0 := signr_eq0.
Definition mulr_sign := mulr_sign.
Definition signr_addb := signr_addb.
Definition signrN := signrN.
Definition signrE := signrE.
Definition mulr_signM := mulr_signM.
Definition exprNn := exprNn.
Definition sqrrN := sqrrN.
Definition sqrr_sign := sqrr_sign.
Definition signrMK := signrMK.
Definition mulrI_eq0 := mulrI_eq0.
Definition lreg_neq0 := lreg_neq0.
Definition mulrI0_lreg := mulrI0_lreg.
Definition lregN := lregN.
Definition lreg1 := lreg1.
Definition lregM := lregM.
Definition lregX := lregX.
Definition lreg_sign := lreg_sign.
Definition lregP {R x} := @lregP R x.
Definition mulIr_eq0 := mulIr_eq0.
Definition mulIr0_rreg := mulIr0_rreg.
Definition rreg_neq0 := rreg_neq0.
Definition rregN := rregN.
Definition rreg1 := rreg1.
Definition rregM := rregM.
Definition revrX := revrX.
Definition rregX := rregX.
Definition rregP {R x} := @rregP R x.
Definition exprDn_comm := exprDn_comm.
Definition exprBn_comm := exprBn_comm.
Definition subrXX_comm := subrXX_comm.
Definition exprD1n := exprD1n.
Definition subrX1 := subrX1.
Definition sqrrD1 := sqrrD1.
Definition sqrrB1 := sqrrB1.
Definition subr_sqr_1 := subr_sqr_1.
Definition charf0 := charf0.
Definition charf_prime := charf_prime.
Definition mulrn_char := mulrn_char.
Definition dvdn_charf := dvdn_charf.
Definition charf_eq := charf_eq.
Definition bin_lt_charf_0 := bin_lt_charf_0.
Definition Frobenius_autE := Frobenius_autE.
Definition Frobenius_aut0 := Frobenius_aut0.
Definition Frobenius_aut1 := Frobenius_aut1.
Definition Frobenius_autD_comm := Frobenius_autD_comm.
Definition Frobenius_autMn := Frobenius_autMn.
Definition Frobenius_aut_nat := Frobenius_aut_nat.
Definition Frobenius_autM_comm := Frobenius_autM_comm.
Definition Frobenius_autX := Frobenius_autX.
Definition Frobenius_autN := Frobenius_autN.
Definition Frobenius_autB_comm := Frobenius_autB_comm.
Definition exprNn_char := exprNn_char.
Definition addrr_char2 := addrr_char2.
Definition oppr_char2 := oppr_char2.
Definition addrK_char2 := addrK_char2.
Definition addKr_char2 := addKr_char2.
Definition iter_mulr := iter_mulr.
Definition iter_mulr_1 := iter_mulr_1.
Definition prodr_const := prodr_const.
Definition prodr_const_nat := prodr_const_nat.
Definition mulrC := mulrC.
Definition mulrCA := mulrCA.
Definition mulrAC := mulrAC.
Definition mulrACA := mulrACA.
Definition exprMn := exprMn.
Definition prodrXl := prodrXl.
Definition prodrXr := prodrXr.
Definition prodrN := prodrN.
Definition prodrMn_const := prodrMn_const.
Definition prodrMn := prodrMn.
Definition natr_prod := natr_prod.
Definition prodr_undup_exp_count := prodr_undup_exp_count.
Definition exprDn := exprDn.
Definition exprBn := exprBn.
Definition subrXX := subrXX.
Definition sqrrD := sqrrD.
Definition sqrrB := sqrrB.
Definition subr_sqr := subr_sqr.
Definition subr_sqrDB := subr_sqrDB.
Definition exprDn_char := exprDn_char.
Definition mulrV := mulrV.
Definition divrr := divrr.
Definition mulVr := mulVr.
Definition invr_out := invr_out.
Definition unitrP {R x} := @unitrP R x.
Definition mulKr := mulKr.
Definition mulVKr := mulVKr.
Definition mulrK := mulrK.
Definition mulrVK := mulrVK.
Definition divrK := divrK.
Definition mulrI := mulrI.
Definition mulIr := mulIr.
Definition divrI := divrI.
Definition divIr := divIr.
Definition telescope_prodr := telescope_prodr.
Definition telescope_prodr_eq := @telescope_prodr_eq.
Arguments telescope_prodr_eq {R n m} f u.
Definition commrV := commrV.
Definition unitrE := unitrE.
Definition invrK := @invrK.
Arguments invrK {R}.
Definition invr_inj := @invr_inj.
Arguments invr_inj {R} [x1 x2].
Definition unitrV := unitrV.
Definition unitr1 := unitr1.
Definition invr1 := invr1.
Definition divr1 := divr1.
Definition div1r := div1r.
Definition natr_div := natr_div.
Definition unitr0 := unitr0.
Definition invr0 := invr0.
Definition unitrN1 := unitrN1.
Definition unitrN := unitrN.
Definition invrN1 := invrN1.
Definition invrN := invrN.
Definition divrNN := divrNN.
Definition divrN := divrN.
Definition invr_sign := invr_sign.
Definition unitrMl := unitrMl.
Definition unitrMr := unitrMr.
Definition invrM := invrM.
Definition invr_eq0 := invr_eq0.
Definition invr_eq1 := invr_eq1.
Definition invr_neq0 := invr_neq0.
Definition unitrM_comm := unitrM_comm.
Definition unitrX := unitrX.
Definition unitrX_pos := unitrX_pos.
Definition exprVn := exprVn.
Definition exprB := exprB.
Definition invr_signM := invr_signM.
Definition divr_signM := divr_signM.
Definition rpred0D := rpred0D.
Definition rpred0 := rpred0.
Definition rpredD := rpredD.
Definition rpredNr := rpredNr.
Definition rpred_sum := rpred_sum.
Definition rpredMn := rpredMn.
Definition rpredN := rpredN.
Definition rpredB := rpredB.
Definition rpredBC := rpredBC.
Definition rpredMNn := rpredMNn.
Definition rpredDr := rpredDr.
Definition rpredDl := rpredDl.
Definition rpredBr := rpredBr.
Definition rpredBl := rpredBl.
Definition rpredMsign := rpredMsign.
Definition rpred1M := rpred1M.
Definition rpred1 := rpred1.
Definition rpredM := rpredM.
Definition rpred_prod := rpred_prod.
Definition rpredX := rpredX.
Definition rpred_nat := rpred_nat.
Definition rpredN1 := rpredN1.
Definition rpred_sign := rpred_sign.
Definition rpredZsign := rpredZsign.
Definition rpredZnat := rpredZnat.
Definition rpredZ := rpredZ.
Definition rpredVr := rpredVr.
Definition rpredV := rpredV.
Definition rpred_div := rpred_div.
Definition rpredXN := rpredXN.
Definition rpredZeq := rpredZeq.
Definition char_lalg := char_lalg.
Definition rpredMr := rpredMr.
Definition rpredMl := rpredMl.
Definition rpred_divr := rpred_divr.
Definition rpred_divl := rpred_divl.
Definition eq_eval := eq_eval.
Definition eval_tsubst := eval_tsubst.
Definition eq_holds := eq_holds.
Definition holds_fsubst := holds_fsubst.
Definition unitrM := unitrM.
Definition unitrPr {R x} := @unitrPr R x.
Definition expr_div_n := expr_div_n.
Definition mulr1_eq := mulr1_eq.
Definition divr1_eq := divr1_eq.
Definition divKr := divKr.
Definition mulf_eq0 := mulf_eq0.
Definition prodf_eq0 := prodf_eq0.
Definition prodf_seq_eq0 := prodf_seq_eq0.
Definition mulf_neq0 := mulf_neq0.
Definition prodf_neq0 := prodf_neq0.
Definition prodf_seq_neq0 := prodf_seq_neq0.
Definition expf_eq0 := expf_eq0.
Definition sqrf_eq0 := sqrf_eq0.
Definition expf_neq0 := expf_neq0.
Definition natf_neq0 := natf_neq0.
Definition natf0_char := natf0_char.
Definition charf'_nat := charf'_nat.
Definition charf0P := charf0P.
Definition eqf_sqr := eqf_sqr.
Definition mulfI := mulfI.
Definition mulIf := mulIf.
Definition divfI := divfI.
Definition divIf := divIf.
Definition sqrf_eq1 := sqrf_eq1.
Definition expfS_eq1 := expfS_eq1.
Definition fieldP := fieldP.
Definition unitfE := unitfE.
Definition mulVf := mulVf.
Definition mulfV := mulfV.
Definition divff := divff.
Definition mulKf := mulKf.
Definition mulVKf := mulVKf.
Definition mulfK := mulfK.
Definition mulfVK := mulfVK.
Definition divfK := divfK.
Definition divKf := divKf.
Definition invfM := invfM.
Definition invf_div := invf_div.
Definition expfB_cond := expfB_cond.
Definition expfB := expfB.
Definition prodfV := prodfV.
Definition prodf_div := prodf_div.
Definition telescope_prodf := telescope_prodf.
Definition telescope_prodf_eq := @telescope_prodf_eq.
Arguments telescope_prodf_eq {F n m} f u.
Definition addf_div := addf_div.
Definition mulf_div := mulf_div.
Definition eqr_div := eqr_div.
Definition eqr_sum_div := eqr_sum_div.
Definition char0_natf_div := char0_natf_div.
Definition fpredMr := fpredMr.
Definition fpredMl := fpredMl.
Definition fpred_divr := fpred_divr.
Definition fpred_divl := fpred_divl.
Definition satP {F e f} := @satP F e f.
Definition eq_sat := eq_sat.
Definition solP {F n f} := @solP F n f.
Definition eq_sol := eq_sol.
Definition size_sol := size_sol.
Definition solve_monicpoly := solve_monicpoly.
Definition raddf0 := raddf0.
Definition raddf_eq0 := raddf_eq0.
Definition raddf_inj := raddf_inj.
Definition raddfN := raddfN.
Definition raddfD := raddfD.
Definition raddfB := raddfB.
Definition raddf_sum := raddf_sum.
Definition raddfMn := raddfMn.
Definition raddfMNn := raddfMNn.
Definition raddfMnat := raddfMnat.
Definition raddfMsign := raddfMsign.
Definition can2_additive := can2_additive.
Definition bij_additive := bij_additive.
Definition rmorph0 := rmorph0.
Definition rmorphN := rmorphN.
Definition rmorphD := rmorphD.
Definition rmorphB := rmorphB.
Definition rmorph_sum := rmorph_sum.
Definition rmorphMn := rmorphMn.
Definition rmorphMNn := rmorphMNn.
Definition rmorphismP := rmorphismP.
Definition rmorphismMP := rmorphismMP.
Definition rmorph1 := rmorph1.
Definition rmorph_eq1 := rmorph_eq1.
Definition rmorphM := rmorphM.
Definition rmorphMsign := rmorphMsign.
Definition rmorph_nat := rmorph_nat.
Definition rmorph_eq_nat := rmorph_eq_nat.
Definition rmorph_prod := rmorph_prod.
Definition rmorphX := rmorphX.
Definition rmorphN1 := rmorphN1.
Definition rmorph_sign := rmorph_sign.
Definition rmorph_char := rmorph_char.
Definition can2_rmorphism := can2_rmorphism.
Definition bij_rmorphism := bij_rmorphism.
Definition rmorph_comm := rmorph_comm.
Definition rmorph_unit := rmorph_unit.
Definition rmorphV := rmorphV.
Definition rmorph_div := rmorph_div.
Definition fmorph_eq0 := fmorph_eq0.
Definition fmorph_inj := @fmorph_inj.
Arguments fmorph_inj {F R} f [x1 x2].
Definition fmorph_eq := fmorph_eq.
Definition fmorph_eq1 := fmorph_eq1.
Definition fmorph_char := fmorph_char.
Definition fmorph_unit := fmorph_unit.
Definition fmorphV := fmorphV.
Definition fmorph_div := fmorph_div.
Definition scalerA := scalerA.
Definition scale1r := scale1r.
Definition scalerDr := scalerDr.
Definition scalerDl := scalerDl.
Definition scaler0 := scaler0.
Definition scale0r := scale0r.
Definition scaleNr := scaleNr.
Definition scaleN1r := scaleN1r.
Definition scalerN := scalerN.
Definition scalerBl := scalerBl.
Definition scalerBr := scalerBr.
Definition scaler_nat := scaler_nat.
Definition scalerMnl := scalerMnl.
Definition scalerMnr := scalerMnr.
Definition scaler_suml := scaler_suml.
Definition scaler_sumr := scaler_sumr.
Definition scaler_eq0 := scaler_eq0.
Definition scalerK := scalerK.
Definition scalerKV := scalerKV.
Definition scalerI := scalerI.
Definition scalerAl := scalerAl.
Definition mulr_algl := mulr_algl.
Definition scaler_sign := scaler_sign.
Definition signrZK := signrZK.
Definition scalerCA := scalerCA.
Definition scalerAr := scalerAr.
Definition mulr_algr := mulr_algr.
Definition comm_alg := comm_alg.
Definition exprZn := exprZn.
Definition scaler_prodl := scaler_prodl.
Definition scaler_prodr := scaler_prodr.
Definition scaler_prod := scaler_prod.
Definition scaler_injl := scaler_injl.
Definition scaler_unit := scaler_unit.
Definition invrZ := invrZ.
Definition raddfZnat := raddfZnat.
Definition raddfZsign := raddfZsign.
Definition in_algE := in_algE.
Definition linear0 := linear0.
Definition linearN := linearN.
Definition linearD := linearD.
Definition linearB := linearB.
Definition linear_sum := linear_sum.
Definition linearMn := linearMn.
Definition linearMNn := linearMNn.
Definition linearP := linearP.
Definition linearZ_LR := linearZ_LR.
Definition linearZ := linearZ.
Definition linearPZ := linearPZ.
Definition linearZZ := linearZZ.
Definition scalarP := scalarP.
Definition scalarZ := scalarZ.
Definition can2_linear := can2_linear.
Definition bij_linear := bij_linear.
Definition rmorph_alg := rmorph_alg.
Definition lrmorphismP := lrmorphismP.
Definition can2_lrmorphism := can2_lrmorphism.
Definition bij_lrmorphism := bij_lrmorphism.
Definition imaginary_exists := imaginary_exists.

Definition raddf := (raddf0, raddfN, raddfD, raddfMn).

Definition rmorphE :=
  (rmorphD, rmorph0, rmorphB, rmorphN, rmorphMNn, rmorphMn, rmorph1, rmorphX).

Definition linearE :=
  (linearD, linear0, linearB, linearMNn, linearMn, linearZ).

Notation null_fun V := (null_fun V) (only parsing).
Notation in_alg A := (in_alg_loc A).

End Theory.

Notation in_alg A := (in_alg_loc A).

End GRing.

Export Zmodule.Exports Ring.Exports Lmodule.Exports Lalgebra.Exports.
Export Additive.Exports RMorphism.Exports Linear.Exports LRMorphism.Exports.
Export Algebra.Exports UnitRing.Exports UnitAlgebra.Exports.
Export ComRing.Exports ComAlgebra.Exports ComUnitRing.Exports.
Export ComUnitAlgebra.Exports IntegralDomain.Exports Field.Exports.
Export DecidableField.Exports ClosedField.Exports.
Export Pred.Exports SubType.Exports.
Notation QEdecFieldMixin := QEdecFieldMixin.

Variant Ione := IOne : Ione.
Variant Inatmul := INatmul : Ione nat Inatmul.
Variant Idummy_placeholder :=.

Definition parse (x : Number.uint) : Inatmul :=
  INatmul IOne (Nat.of_num_uint x).

Definition print (x : Inatmul) : Number.uint :=
  match x with
  | INatmul IOne nNumber.UIntDecimal (Nat.to_uint n)
  end.

Arguments GRing.one {R}.
Arguments GRing.one : clear implicits.

Notation "0" := (zero _) : ring_scope.
Notation "-%R" := (@opp _) : fun_scope.
Notation "- x" := (opp x) : ring_scope.
Notation "+%R" := (@add _) : fun_scope.
Notation "x + y" := (add x y) : ring_scope.
Notation "x - y" := (add x (- y)) : ring_scope.
Notation "x *+ n" := (natmul x n) : ring_scope.
Notation "x *- n" := (opp (x *+ n)) : ring_scope.
Notation "s `_ i" := (seq.nth 0%R s%R i) : ring_scope.
Notation support := 0.-support.

Notation "1" := (one _) : ring_scope.
Notation "- 1" := (opp 1) : ring_scope.

Notation "n %:R" := (natmul 1 n) : ring_scope.
Notation "[ 'char' R ]" := (char (Phant R)) : ring_scope.
Notation Frobenius_aut chRp := (Frobenius_aut chRp).
Notation "*%R" := (@mul _) : fun_scope.
Notation "x * y" := (mul x y) : ring_scope.
Notation "x ^+ n" := (exp x n) : ring_scope.
Notation "x ^-1" := (inv x) : ring_scope.
Notation "x ^- n" := (inv (x ^+ n)) : ring_scope.
Notation "x / y" := (mul x y^-1) : ring_scope.

Notation "*:%R" := (@scale _ _) : fun_scope.
Notation "a *: m" := (scale a m) : ring_scope.
Notation "k %:A" := (scale k 1) : ring_scope.
Notation "\0" := (null_fun _) : ring_scope.
Notation "f \+ g" := (add_fun f g) : ring_scope.
Notation "f \- g" := (sub_fun f g) : ring_scope.
Notation "\- f" := (opp_fun f) : ring_scope.
Notation "a \*: f" := (scale_fun a f) : ring_scope.
Notation "x \*o f" := (mull_fun x f) : ring_scope.
Notation "x \o* f" := (mulr_fun x f) : ring_scope.
Notation "f \* g" := (mul_fun f g) : ring_scope.

Arguments add_fun {_ _} f g _ /.
Arguments sub_fun {_ _} f g _ /.
Arguments opp_fun {_ _} f _ /.
Arguments mull_fun {_ _} a f _ /.
Arguments mulr_fun {_ _} a f _ /.
Arguments scale_fun {_ _ _} a f _ /.
Arguments mul_fun {_ _} f g _ /.

Notation "\sum_ ( i <- r | P ) F" :=
  (\big[+%R/0%R]_(i <- r | P%B) F%R) : ring_scope.
Notation "\sum_ ( i <- r ) F" :=
  (\big[+%R/0%R]_(i <- r) F%R) : ring_scope.
Notation "\sum_ ( m <= i < n | P ) F" :=
  (\big[+%R/0%R]_(m i < n | P%B) F%R) : ring_scope.
Notation "\sum_ ( m <= i < n ) F" :=
  (\big[+%R/0%R]_(m i < n) F%R) : ring_scope.
Notation "\sum_ ( i | P ) F" :=
  (\big[+%R/0%R]_(i | P%B) F%R) : ring_scope.
Notation "\sum_ i F" :=
  (\big[+%R/0%R]_i F%R) : ring_scope.
Notation "\sum_ ( i : t | P ) F" :=
  (\big[+%R/0%R]_(i : t | P%B) F%R) (only parsing) : ring_scope.
Notation "\sum_ ( i : t ) F" :=
  (\big[+%R/0%R]_(i : t) F%R) (only parsing) : ring_scope.
Notation "\sum_ ( i < n | P ) F" :=
  (\big[+%R/0%R]_(i < n | P%B) F%R) : ring_scope.
Notation "\sum_ ( i < n ) F" :=
  (\big[+%R/0%R]_(i < n) F%R) : ring_scope.
Notation "\sum_ ( i 'in' A | P ) F" :=
  (\big[+%R/0%R]_(i in A | P%B) F%R) : ring_scope.
Notation "\sum_ ( i 'in' A ) F" :=
  (\big[+%R/0%R]_(i in A) F%R) : ring_scope.

Notation "\prod_ ( i <- r | P ) F" :=
  (\big[*%R/1%R]_(i <- r | P%B) F%R) : ring_scope.
Notation "\prod_ ( i <- r ) F" :=
  (\big[*%R/1%R]_(i <- r) F%R) : ring_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
  (\big[*%R/1%R]_(m i < n | P%B) F%R) : ring_scope.
Notation "\prod_ ( m <= i < n ) F" :=
  (\big[*%R/1%R]_(m i < n) F%R) : ring_scope.
Notation "\prod_ ( i | P ) F" :=
  (\big[*%R/1%R]_(i | P%B) F%R) : ring_scope.
Notation "\prod_ i F" :=
  (\big[*%R/1%R]_i F%R) : ring_scope.
Notation "\prod_ ( i : t | P ) F" :=
  (\big[*%R/1%R]_(i : t | P%B) F%R) (only parsing) : ring_scope.
Notation "\prod_ ( i : t ) F" :=
  (\big[*%R/1%R]_(i : t) F%R) (only parsing) : ring_scope.
Notation "\prod_ ( i < n | P ) F" :=
  (\big[*%R/1%R]_(i < n | P%B) F%R) : ring_scope.
Notation "\prod_ ( i < n ) F" :=
  (\big[*%R/1%R]_(i < n) F%R) : ring_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
  (\big[*%R/1%R]_(i in A | P%B) F%R) : ring_scope.
Notation "\prod_ ( i 'in' A ) F" :=
  (\big[*%R/1%R]_(i in A) F%R) : ring_scope.

Canonical add_monoid.
Canonical add_comoid.
Canonical mul_monoid.
Canonical mul_comoid.
Canonical muloid.
Canonical addoid.

Canonical locked_additive.
Canonical locked_rmorphism.
Canonical locked_linear.
Canonical locked_lrmorphism.
Canonical idfun_additive.
Canonical idfun_rmorphism.
Canonical idfun_linear.
Canonical idfun_lrmorphism.
Canonical comp_additive.
Canonical comp_rmorphism.
Canonical comp_linear.
Canonical comp_lrmorphism.
Canonical opp_additive.
Canonical opp_linear.
Canonical scale_additive.
Canonical scale_linear.
Canonical null_fun_additive.
Canonical null_fun_linear.
Canonical scale_fun_additive.
Canonical scale_fun_linear.
Canonical add_fun_additive.
Canonical add_fun_linear.
Canonical sub_fun_additive.
Canonical sub_fun_linear.
Canonical opp_fun_additive.
Canonical opp_fun_linear.
Canonical mull_fun_additive.
Canonical mull_fun_linear.
Canonical mulr_fun_additive.
Canonical mulr_fun_linear.
Canonical Frobenius_aut_additive.
Canonical Frobenius_aut_rmorphism.
Canonical in_alg_additive.
Canonical in_alg_rmorphism.

Notation "R ^c" := (converse R) (at level 2, format "R ^c") : type_scope.
Canonical converse_eqType.
Canonical converse_choiceType.
Canonical converse_zmodType.
Canonical converse_ringType.
Canonical converse_unitRingType.

Notation "R ^o" := (regular R) (at level 2, format "R ^o") : type_scope.
Canonical regular_eqType.
Canonical regular_choiceType.
Canonical regular_zmodType.
Canonical regular_ringType.
Canonical regular_lmodType.
Canonical regular_lalgType.
Canonical regular_comRingType.
Canonical regular_algType.
Canonical regular_unitRingType.
Canonical regular_comUnitRingType.
Canonical regular_unitAlgType.
Canonical regular_comAlgType.
Canonical regular_comUnitAlgType.
Canonical regular_idomainType.
Canonical regular_fieldType.

Canonical unit_keyed.
Canonical unit_opprPred.
Canonical unit_mulrPred.
Canonical unit_smulrPred.
Canonical unit_divrPred.
Canonical unit_sdivrPred.

Bind Scope term_scope with term.
Bind Scope term_scope with formula.

Notation "''X_' i" := (Var _ i) : term_scope.
Notation "n %:R" := (NatConst _ n) : term_scope.
Notation "0" := 0%:R%T : term_scope.
Notation "1" := 1%:R%T : term_scope.
Notation "x %:T" := (Const x) : term_scope.
Infix "+" := Add : term_scope.
Notation "- t" := (Opp t) : term_scope.
Notation "t - u" := (Add t (- u)) : term_scope.
Infix "×" := Mul : term_scope.
Infix "*+" := NatMul : term_scope.
Notation "t ^-1" := (Inv t) : term_scope.
Notation "t / u" := (Mul t u^-1) : term_scope.
Infix "^+" := Exp : term_scope.
Infix "==" := Equal : term_scope.
Notation "x != y" := (GRing.Not (x == y)) : term_scope.
Infix "∧" := And : term_scope.
Infix "∨" := Or : term_scope.
Infix "==>" := Implies : term_scope.
Notation "~ f" := (Not f) : term_scope.
Notation "''exists' ''X_' i , f" := (Exists i f) : term_scope.
Notation "''forall' ''X_' i , f" := (Forall i f) : term_scope.

Lifting Structure from the codomain of finfuns.
Section FinFunZmod.

Variable (aT : finType) (rT : zmodType).
Implicit Types f g : {ffun aT rT}.

Definition ffun_zero := [ffun a : aT (0 : rT)].
Definition ffun_opp f := [ffun a - f a].
Definition ffun_add f g := [ffun a f a + g a].

Fact ffun_addA : associative ffun_add.
Fact ffun_addC : commutative ffun_add.
Fact ffun_add0 : left_id ffun_zero ffun_add.
Fact ffun_addN : left_inverse ffun_zero ffun_opp ffun_add.

Definition ffun_zmodMixin :=
  Zmodule.Mixin ffun_addA ffun_addC ffun_add0 ffun_addN.
Canonical ffun_zmodType := Eval hnf in ZmodType _ ffun_zmodMixin.

Section Sum.

Variables (I : Type) (r : seq I) (P : pred I) (F : I {ffun aT rT}).

Lemma sum_ffunE x : (\sum_(i <- r | P i) F i) x = \sum_(i <- r | P i) F i x.

Lemma sum_ffun :
  \sum_(i <- r | P i) F i = [ffun x \sum_(i <- r | P i) F i x].

End Sum.

Lemma ffunMnE f n x : (f *+ n) x = f x *+ n.

End FinFunZmod.

Section FinFunRing.

As rings require 1 != 0 in order to lift a ring structure over finfuns we need evidence that the domain is non-empty.

Variable (aT : finType) (R : ringType) (a : aT).

Definition ffun_one : {ffun aT R} := [ffun 1].
Definition ffun_mul (f g : {ffun aT R}) := [ffun x f x × g x].

Fact ffun_mulA : associative ffun_mul.
Fact ffun_mul_1l : left_id ffun_one ffun_mul.
Fact ffun_mul_1r : right_id ffun_one ffun_mul.
Fact ffun_mul_addl : left_distributive ffun_mul (@ffun_add _ _).
Fact ffun_mul_addr : right_distributive ffun_mul (@ffun_add _ _).
Fact ffun1_nonzero : ffun_one != 0.

Definition ffun_ringMixin :=
  RingMixin ffun_mulA ffun_mul_1l ffun_mul_1r ffun_mul_addl ffun_mul_addr
            ffun1_nonzero.
Definition ffun_ringType :=
  Eval hnf in RingType {ffun aT R} ffun_ringMixin.

End FinFunRing.

Section FinFunComRing.

Variable (aT : finType) (R : comRingType) (a : aT).

Fact ffun_mulC : commutative (@ffun_mul aT R).

Definition ffun_comRingType :=
  Eval hnf in ComRingType (ffun_ringType R a) ffun_mulC.

End FinFunComRing.

Section FinFunLmod.

Variable (R : ringType) (aT : finType) (rT : lmodType R).

Implicit Types f g : {ffun aT rT}.

Definition ffun_scale k f := [ffun a k *: f a].

Fact ffun_scaleA k1 k2 f :
  ffun_scale k1 (ffun_scale k2 f) = ffun_scale (k1 × k2) f.
Fact ffun_scale1 : left_id 1 ffun_scale.
Fact ffun_scale_addr k : {morph (ffun_scale k) : x y / x + y}.
Fact ffun_scale_addl u : {morph (ffun_scale)^~ u : k1 k2 / k1 + k2}.

Definition ffun_lmodMixin :=
  LmodMixin ffun_scaleA ffun_scale1 ffun_scale_addr ffun_scale_addl.
Canonical ffun_lmodType :=
  Eval hnf in LmodType R {ffun aT rT} ffun_lmodMixin.

End FinFunLmod.

External direct product.
Section PairZmod.

Variables M1 M2 : zmodType.

Definition opp_pair (x : M1 × M2) := (- x.1, - x.2).
Definition add_pair (x y : M1 × M2) := (x.1 + y.1, x.2 + y.2).

Fact pair_addA : associative add_pair.

Fact pair_addC : commutative add_pair.

Fact pair_add0 : left_id (0, 0) add_pair.

Fact pair_addN : left_inverse (0, 0) opp_pair add_pair.

Definition pair_zmodMixin := ZmodMixin pair_addA pair_addC pair_add0 pair_addN.
Canonical pair_zmodType := Eval hnf in ZmodType (M1 × M2) pair_zmodMixin.

Fact fst_is_additive : additive fst.
Canonical fst_additive := Additive fst_is_additive.
Fact snd_is_additive : additive snd.
Canonical snd_additive := Additive snd_is_additive.

End PairZmod.

Section PairRing.

Variables R1 R2 : ringType.

Definition mul_pair (x y : R1 × R2) := (x.1 × y.1, x.2 × y.2).

Fact pair_mulA : associative mul_pair.

Fact pair_mul1l : left_id (1, 1) mul_pair.

Fact pair_mul1r : right_id (1, 1) mul_pair.

Fact pair_mulDl : left_distributive mul_pair +%R.

Fact pair_mulDr : right_distributive mul_pair +%R.

Fact pair_one_neq0 : (1, 1) != 0 :> R1 × R2.

Definition pair_ringMixin :=
  RingMixin pair_mulA pair_mul1l pair_mul1r pair_mulDl pair_mulDr pair_one_neq0.
Canonical pair_ringType := Eval hnf in RingType (R1 × R2) pair_ringMixin.

Fact fst_is_multiplicative : multiplicative fst.
Canonical fst_rmorphism := AddRMorphism fst_is_multiplicative.
Fact snd_is_multiplicative : multiplicative snd.
Canonical snd_rmorphism := AddRMorphism snd_is_multiplicative.

End PairRing.

Section PairComRing.

Variables R1 R2 : comRingType.

Fact pair_mulC : commutative (@mul_pair R1 R2).

Canonical pair_comRingType := Eval hnf in ComRingType (R1 × R2) pair_mulC.

End PairComRing.

Section PairLmod.

Variables (R : ringType) (V1 V2 : lmodType R).

Definition scale_pair a (v : V1 × V2) : V1 × V2 := (a *: v.1, a *: v.2).

Fact pair_scaleA a b u : scale_pair a (scale_pair b u) = scale_pair (a × b) u.

Fact pair_scale1 u : scale_pair 1 u = u.

Fact pair_scaleDr : right_distributive scale_pair +%R.

Fact pair_scaleDl u : {morph scale_pair^~ u: a b / a + b}.

Definition pair_lmodMixin :=
  LmodMixin pair_scaleA pair_scale1 pair_scaleDr pair_scaleDl.
Canonical pair_lmodType := Eval hnf in LmodType R (V1 × V2) pair_lmodMixin.

Fact fst_is_scalable : scalable fst.
Canonical fst_linear := AddLinear fst_is_scalable.
Fact snd_is_scalable : scalable snd.
Canonical snd_linear := AddLinear snd_is_scalable.

End PairLmod.

Section PairLalg.

Variables (R : ringType) (A1 A2 : lalgType R).

Fact pair_scaleAl a (u v : A1 × A2) : a *: (u × v) = (a *: u) × v.
Canonical pair_lalgType := Eval hnf in LalgType R (A1 × A2) pair_scaleAl.

Definition fst_lrmorphism := [lrmorphism of fst].
Definition snd_lrmorphism := [lrmorphism of snd].

End PairLalg.

Section PairAlg.

Variables (R : comRingType) (A1 A2 : algType R).

Fact pair_scaleAr a (u v : A1 × A2) : a *: (u × v) = u × (a *: v).
Canonical pair_algType := Eval hnf in AlgType R (A1 × A2) pair_scaleAr.

End PairAlg.

Section PairUnitRing.

Variables R1 R2 : unitRingType.

Definition pair_unitr :=
  [qualify a x : R1 × R2 | (x.1 \is a GRing.unit) && (x.2 \is a GRing.unit)].
Definition pair_invr x :=
  if x \is a pair_unitr then (x.1^-1, x.2^-1) else x.

Lemma pair_mulVl : {in pair_unitr, left_inverse 1 pair_invr *%R}.

Lemma pair_mulVr : {in pair_unitr, right_inverse 1 pair_invr *%R}.

Lemma pair_unitP x y : y × x = 1 x × y = 1 x \is a pair_unitr.

Lemma pair_invr_out : {in [predC pair_unitr], pair_invr =1 id}.

Definition pair_unitRingMixin :=
  UnitRingMixin pair_mulVl pair_mulVr pair_unitP pair_invr_out.
Canonical pair_unitRingType :=
  Eval hnf in UnitRingType (R1 × R2) pair_unitRingMixin.

End PairUnitRing.

Canonical pair_comUnitRingType (R1 R2 : comUnitRingType) :=
  Eval hnf in [comUnitRingType of R1 × R2].

Canonical pair_unitAlgType (R : comUnitRingType) (A1 A2 : unitAlgType R) :=
  Eval hnf in [unitAlgType R of A1 × A2].

Lemma pairMnE (M1 M2 : zmodType) (x : M1 × M2) n :
  x *+ n = (x.1 *+ n, x.2 *+ n).