Require Export equiv.
Require Export abgroup.

Require quot.

Implicit Arguments On.

Module AbGroup_Quot.

Export Quot.
Export AbGroup.

Record Compatible_Group [A:Group_Data; Q:(Equivalence A)] : Prop := {
  add_compatible : (Compatible2 Q Q [x,y:A](class Q (add x y)));
  opp_compatible : (Compatible Q [x:A](class Q (opp x)))
 }.

Section Group_Quot.

Variable A:Group; Q:(Equivalence A); HQ:(Compatible_Group Q).

Definition class_eq_Q := (!class_eq ? Q).

Hints Resolve class_eq_Q.

Local B := (quot Q).

Local Bop : B->B->B.
Proof.
  Apply (quot_law2 Q (!add A)).
  Abstract NewDestruct HQ; Trivial.
Defined.

Local Bid : B := (class Q (!zero A)).

Local Biv : B->B.
Proof.
  Apply (quot_law Q (!opp A)).
  Abstract NewDestruct HQ; Trivial.
Defined.

Local B_data : Group_Data := (Build_Group_Data Bop Bid Biv).

Remark B_theory :
 (Group_Theory (!add B_data) (!zero B_data) (!opp B_data)).
Proof.
  Split; Simpl; Unfold Bop Bid Biv; Intros.
  Lift x; Lift y; Lift z; Unfold quot_law2.
  Repeat Rewrite fact2_eq; Auto.
  Lift x; Lift y; Unfold quot_law2.
  Repeat Rewrite fact2_eq; Auto.
  Lift x; Unfold quot_law2; Repeat Rewrite fact2_eq; Auto.
  Lift x; Unfold quot_law2 quot_law.
  Repeat Rewrite fact_eq; Repeat Rewrite fact2_eq; Auto.
Qed.

Definition group_quot : Group.
Proof.
  Split with B_data.
  Exact B_theory.
Defined.

End Group_Quot.