# Library Buchberger.CoefStructure

Require Import Relation_Definitions.

Record CoefStructure (A : Set) (A0 A1 : A) (eqA : A -> A -> Prop)
(plusA : A -> A -> A) (invA : A -> A) (minusA multA : A -> A -> A)
(divA : A -> forall b : A, ~ eqA b A0 -> A) : Prop := mkCoefStructure
{A1_diff_A0 : ~ eqA A1 A0;
eqA_ref : reflexive A eqA;
eqA_sym : symmetric A eqA;
eqA_trans : transitive A eqA;
plusA_assoc :
forall a b c : A, eqA (plusA a (plusA b c)) (plusA (plusA a b) c);
plusA_com : forall a b : A, eqA (plusA a b) (plusA b a);
plusA_eqA_comp :
forall a b c d : A, eqA a c -> eqA b d -> eqA (plusA a b) (plusA c d);
plusA_A0 : forall a : A, eqA a (plusA a A0);
invA_plusA : forall a : A, eqA A0 (plusA a (invA a));
invA_eqA_comp : forall a b : A, eqA a b -> eqA (invA a) (invA b);
minusA_def : forall a b : A, eqA (minusA a b) (plusA a (invA b));
multA_eqA_comp :
forall a b c d : A, eqA a c -> eqA b d -> eqA (multA a b) (multA c d);
multA_assoc :
forall a b c : A, eqA (multA a (multA b c)) (multA (multA a b) c);
multA_com : forall a b : A, eqA (multA a b) (multA b a);
multA_dist_l :
forall a b c : A,
eqA (plusA (multA c a) (multA c b)) (multA c (plusA a b));
multA_A0_l : forall a : A, eqA (multA A0 a) A0;
multA_A1_l : forall a : A, eqA (multA A1 a) a;
divA_rew :
forall (a b : A) (nZ1 nZ2 : ~ eqA b A0), divA a b nZ1 = divA a b nZ2;
divA_is_multA :
forall (a b : A) (nZb : ~ eqA b A0), eqA a (multA (divA a b nZb) b);
divA_eqA_comp :
forall (a b c d : A) (nZb : ~ eqA b A0) (nZd : ~ eqA d A0),
eqA a c -> eqA b d -> eqA (divA a b nZb) (divA c d nZd);
divA_multA_comp_r :
forall (a b c : A) (nZc : ~ eqA c A0),
eqA (divA (multA a b) c nZc) (multA (divA a c nZc) b);
divA_invA_r :
forall (a b : A) (nZb : ~ eqA b A0) (nZib : ~ eqA (invA b) A0),
eqA (divA a (invA b) nZib) (invA (divA a b nZb))}.