Module abgroup_test

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.


Index
This page has been generated by coqdoc