1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 include "algebra/CSetoids.ma".
21 include "algebra/CSetoidFun.ma".
23 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/ap_fun.con" as definition.
25 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/eq_fun.con" as definition.
27 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/irrefl_apfun.con" as lemma.
29 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/cotrans_apfun.con" as lemma.
31 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/ta_apfun.con" as lemma.
33 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/sym_apfun.con" as lemma.
35 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_is_CSetoid.con" as definition.
37 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSetoid.con" as definition.
43 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/comp.con" as definition.
45 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/comp_as_bin_op.con" as definition.
47 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/assoc_comp.con" as lemma.
49 include "algebra/CSemiGroups.ma".
51 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSemiGroup.con" as definition.
53 include "algebra/CMonoids.ma".
55 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_id.con" as definition.
57 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/id_is_rht_unit.con" as lemma.
59 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/id_is_lft_unit.con" as lemma.
61 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_is_CMonoid.con" as definition.
63 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CMonoid.con" as definition.
65 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_as_CMonoid.con" as definition.
67 include "algebra/CGroups.ma".
69 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/Inv_is_bij.con" as lemma.
72 forall (A B : CSetoid) (f : CSetoid_fun A B) (H : bijective f),
76 unfold fun_strext in |- *.
78 unfold bijective in |- *.
82 unfold injective in |- *.
83 unfold surjective in |- *.
88 unfold invfun in |- *.
90 unfold sigT_rect in |- *.
105 unfold invfun in |- *.
107 unfold sigT_rect in |- *.
118 set (H4 := H0 x b H3) in *.
119 set (H6 := ap_imp_neq B (f0 x) (f0 b) H4) in *.
123 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_Inv.con" as definition.
125 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/Inv_as_un_op.con" as definition.
127 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_is_CGroup.con" as lemma.
129 inline procedural "cic:/CoRN/devel/loeb/per/csetfun/PS_as_CGroup.con" as definition.
131 (* In het algemeen niet Abels! *)