Require Export equiv.
Require Export cmonoid.

Require quot.

Implicit Arguments On.

Module CMonoid_Quot.

Export Quot.
Export CMonoid.

Definition Compatible_Monoid [A:Monoid; Q:(Equivalence A)] : Prop :=
  (Compatible2 Q Q [x,y:A](class Q (mul x y))).

Section Monoid_Quot.

Variable A:Monoid; Q:(Equivalence A); HQ:(Compatible_Monoid 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 (!mul A)); Auto.
Defined.

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

Local B_data : Monoid_Data := (Build_Monoid_Data Bop Bid).

Remark B_theory : (Monoid_Theory (!mul B_data) (!one B_data)).
Proof.
  Split; Simpl; Unfold Bop Bid; 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; Repeat Rewrite fact2_eq; Auto.
Qed.

Definition monoid_quot : Monoid.
Proof.
  Split with B_data.
  Exact B_theory.
Defined.

End Monoid_Quot.