| Time-stamp: "2002-08-19 11:56:14 maggesi" |
Require Export abgroup.
Implicit Arguments On.
Section test.
Variable A : Type.
Variable op : A->A->A.
Variable id : A.
Variable iv : A->A.
Variable AB : (CGroup_Theory op id iv).
Variables a, b: A.
Remark test1 :
(op (op id a) (op b a))==(op (op a (op b a)) (op b (iv b))).
Proof.
AbGroup1 op id iv AB '(op (op id a) (op b a)).
AbGroup1 op id iv AB '(op (op a (op b a)) (op b (iv b))).
Reflexivity.
Qed.
Remark test2 :
(op (op id a) (op b a))==(op (op a (op b a)) (op b (iv b))).
Proof.
AbGroup op id iv AB.
Qed.
Remark test3 :
(op a b)==(op b a).
Proof.
AbGroup op id iv AB.
Qed.
End test.
Section test2.
Variable A : CGroup.
Variables a, b, c : A.
Remark test1 :
(add (add (zero A) a) (add b a))==(add (add a (add b a)) (add b (opp b))).
Proof.
CGroup1 '(add (add (zero A) a) (add b a)).
CGroup1 '(add (add a (add b a)) (add b (opp b))).
Reflexivity.
Qed.
Remark test2 :
(add (add (zero A) a) (add b a))==(add (add a (add b a)) (add b (opp b))).
Proof.
CGroup A.
Qed.
End test2.