fix

[helm.git] / matita / contribs / CoRN-Decl / algebra / CGroups.ma

diff --git a/matita/contribs/CoRN-Decl/algebra/CGroups.ma b/matita/contribs/CoRN-Decl/algebra/CGroups.ma
index d13953b4173d9589a886eb2109e522d0e2f4fcbb..6e644810bc76db479a5c606ba0da4e6840eb0f87 100644 (file)
--- a/matita/contribs/CoRN-Decl/algebra/CGroups.ma
+++ b/matita/contribs/CoRN-Decl/algebra/CGroups.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups".
 
+include "CoRN.ma".
+
 (* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *)
 
 (*#* printing [-] %\ensuremath-% #−# *)
@@ -26,9 +28,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CGroups".
 
 (*#* printing {--} %\ensuremath-% #−# *)
 
-(* INCLUDE
-CMonoids
-*)
+include "algebra/CMonoids.ma".
 
 (* Begin_SpecReals *)
 
@@ -37,15 +37,17 @@ CMonoids
 ** Definition of the notion of Group
 *)
 
-inline cic:/CoRN/algebra/CGroups/is_inverse.con.
+inline "cic:/CoRN/algebra/CGroups/is_inverse.con".
 
 (* UNEXPORTED
 Implicit Arguments is_inverse [S].
 *)
 
-inline cic:/CoRN/algebra/CGroups/is_CGroup.con.
+inline "cic:/CoRN/algebra/CGroups/is_CGroup.con".
+
+inline "cic:/CoRN/algebra/CGroups/CGroup.ind".
 
-inline cic:/CoRN/algebra/CGroups/CGroup.ind.
+coercion cic:/matita/CoRN-Decl/algebra/CGroups/cg_crr.con 0 (* compounds *).
 
 (* End_SpecReals *)
 
@@ -55,7 +57,11 @@ inline cic:/CoRN/algebra/CGroups/CGroup.ind.
 Implicit Arguments cg_inv [c].
 *)
 
-inline cic:/CoRN/algebra/CGroups/cg_minus.con.
+(* NOTATION
+Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
+*)
+
+inline "cic:/CoRN/algebra/CGroups/cg_minus.con".
 
 (*#*
 %\begin{nameconvention}%
@@ -68,6 +74,10 @@ and [ [-] ] with [minus].
 Implicit Arguments cg_minus [G].
 *)
 
+(* NOTATION
+Infix "[-]" := cg_minus (at level 50, left associativity).
+*)
+
 (* End_SpecReals *)
 
 (*#*
@@ -80,9 +90,9 @@ Implicit Arguments cg_minus [G].
 Section CGroup_axioms.
 *)
 
-inline cic:/CoRN/algebra/CGroups/G.var.
+inline "cic:/CoRN/algebra/CGroups/G.var".
 
-inline cic:/CoRN/algebra/CGroups/cg_inverse.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inverse.con".
 
 (* UNEXPORTED
 End CGroup_axioms.
@@ -99,76 +109,76 @@ General properties of groups.
 Section CGroup_basics.
 *)
 
-inline cic:/CoRN/algebra/CGroups/G.var.
+inline "cic:/CoRN/algebra/CGroups/G.var".
 
-inline cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con.
+inline "cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_lft_inv_unfolded.con.
+inline "cic:/CoRN/algebra/CGroups/cg_lft_inv_unfolded.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_minus_correct.con.
+inline "cic:/CoRN/algebra/CGroups/cg_minus_correct.con".
 
 (* UNEXPORTED
 Hint Resolve cg_rht_inv_unfolded cg_lft_inv_unfolded cg_minus_correct:
   algebra.
 *)
 
-inline cic:/CoRN/algebra/CGroups/cg_inverse'.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inverse'.con".
 
 (* Hints for Auto *)
 
-inline cic:/CoRN/algebra/CGroups/cg_minus_unfolded.con.
+inline "cic:/CoRN/algebra/CGroups/cg_minus_unfolded.con".
 
 (* UNEXPORTED
 Hint Resolve cg_minus_unfolded: algebra.
 *)
 
-inline cic:/CoRN/algebra/CGroups/cg_minus_wd.con.
+inline "cic:/CoRN/algebra/CGroups/cg_minus_wd.con".
 
 (* UNEXPORTED
 Hint Resolve cg_minus_wd: algebra_c.
 *)
 
-inline cic:/CoRN/algebra/CGroups/cg_minus_strext.con.
+inline "cic:/CoRN/algebra/CGroups/cg_minus_strext.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_minus_is_csetoid_bin_op.con.
+inline "cic:/CoRN/algebra/CGroups/cg_minus_is_csetoid_bin_op.con".
 
-inline cic:/CoRN/algebra/CGroups/grp_inv_assoc.con.
+inline "cic:/CoRN/algebra/CGroups/grp_inv_assoc.con".
 
 (* UNEXPORTED
 Hint Resolve grp_inv_assoc: algebra.
 *)
 
-inline cic:/CoRN/algebra/CGroups/cg_inv_unique.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inv_unique.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_inv_inv.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inv_inv.con".
 
 (* UNEXPORTED
 Hint Resolve cg_inv_inv: algebra.
 *)
 
-inline cic:/CoRN/algebra/CGroups/cg_cancel_lft.con.
+inline "cic:/CoRN/algebra/CGroups/cg_cancel_lft.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_cancel_rht.con.
+inline "cic:/CoRN/algebra/CGroups/cg_cancel_rht.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_inv_unique'.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inv_unique'.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_inv_unique_2.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inv_unique_2.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_zero_inv.con.
+inline "cic:/CoRN/algebra/CGroups/cg_zero_inv.con".
 
 (* UNEXPORTED
 Hint Resolve cg_zero_inv: algebra.
 *)
 
-inline cic:/CoRN/algebra/CGroups/cg_inv_zero.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inv_zero.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_inv_op.con.
+inline "cic:/CoRN/algebra/CGroups/cg_inv_op.con".
 
 (*#*
 Useful for interactive proof development.
 *)
 
-inline cic:/CoRN/algebra/CGroups/x_minus_x.con.
+inline "cic:/CoRN/algebra/CGroups/x_minus_x.con".
 
 (*#*
 ** Sub-groups
@@ -181,21 +191,21 @@ inline cic:/CoRN/algebra/CGroups/x_minus_x.con.
 Section SubCGroups.
 *)
 
-inline cic:/CoRN/algebra/CGroups/P.var.
+inline "cic:/CoRN/algebra/CGroups/P.var".
 
-inline cic:/CoRN/algebra/CGroups/Punit.var.
+inline "cic:/CoRN/algebra/CGroups/Punit.var".
 
-inline cic:/CoRN/algebra/CGroups/op_pres_P.var.
+inline "cic:/CoRN/algebra/CGroups/op_pres_P.var".
 
-inline cic:/CoRN/algebra/CGroups/inv_pres_P.var.
+inline "cic:/CoRN/algebra/CGroups/inv_pres_P.var".
 
-inline cic:/CoRN/algebra/CGroups/subcrr.con.
+inline "cic:/CoRN/algebra/CGroups/subcrr.con".
 
-inline cic:/CoRN/algebra/CGroups/subinv.con.
+inline "cic:/CoRN/algebra/CGroups/subinv.con".
 
-inline cic:/CoRN/algebra/CGroups/isgrp_scrr.con.
+inline "cic:/CoRN/algebra/CGroups/isgrp_scrr.con".
 
-inline cic:/CoRN/algebra/CGroups/Build_SubCGroup.con.
+inline "cic:/CoRN/algebra/CGroups/Build_SubCGroup.con".
 
 (* UNEXPORTED
 End SubCGroups.
@@ -231,15 +241,15 @@ Hint Resolve cg_minus_wd: algebra_c.
 Section Assoc_properties.
 *)
 
-inline cic:/CoRN/algebra/CGroups/G.var.
+inline "cic:/CoRN/algebra/CGroups/G.var".
 
-inline cic:/CoRN/algebra/CGroups/assoc_2.con.
+inline "cic:/CoRN/algebra/CGroups/assoc_2.con".
 
-inline cic:/CoRN/algebra/CGroups/zero_minus.con.
+inline "cic:/CoRN/algebra/CGroups/zero_minus.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_cancel_mixed.con.
+inline "cic:/CoRN/algebra/CGroups/cg_cancel_mixed.con".
 
-inline cic:/CoRN/algebra/CGroups/plus_resp_eq.con.
+inline "cic:/CoRN/algebra/CGroups/plus_resp_eq.con".
 
 (* UNEXPORTED
 End Assoc_properties.
@@ -261,29 +271,29 @@ Specific properties of apartness.
 Section cgroups_apartness.
 *)
 
-inline cic:/CoRN/algebra/CGroups/G.var.
+inline "cic:/CoRN/algebra/CGroups/G.var".
 
-inline cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con.
+inline "cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con".
 
-inline cic:/CoRN/algebra/CGroups/op_rht_resp_ap.con.
+inline "cic:/CoRN/algebra/CGroups/op_rht_resp_ap.con".
 
-inline cic:/CoRN/algebra/CGroups/cg_ap_cancel_rht.con.
+inline "cic:/CoRN/algebra/CGroups/cg_ap_cancel_rht.con".
 
-inline cic:/CoRN/algebra/CGroups/plus_cancel_ap_rht.con.
+inline "cic:/CoRN/algebra/CGroups/plus_cancel_ap_rht.con".
 
-inline cic:/CoRN/algebra/CGroups/minus_ap_zero.con.
+inline "cic:/CoRN/algebra/CGroups/minus_ap_zero.con".
 
-inline cic:/CoRN/algebra/CGroups/zero_minus_apart.con.
+inline "cic:/CoRN/algebra/CGroups/zero_minus_apart.con".
 
-inline cic:/CoRN/algebra/CGroups/inv_resp_ap_zero.con.
+inline "cic:/CoRN/algebra/CGroups/inv_resp_ap_zero.con".
 
-inline cic:/CoRN/algebra/CGroups/inv_resp_ap.con.
+inline "cic:/CoRN/algebra/CGroups/inv_resp_ap.con".
 
-inline cic:/CoRN/algebra/CGroups/minus_resp_ap_rht.con.
+inline "cic:/CoRN/algebra/CGroups/minus_resp_ap_rht.con".
 
-inline cic:/CoRN/algebra/CGroups/minus_resp_ap_lft.con.
+inline "cic:/CoRN/algebra/CGroups/minus_resp_ap_lft.con".
 
-inline cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con.
+inline "cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con".
 
 (* UNEXPORTED
 End cgroups_apartness.
@@ -312,17 +322,17 @@ by [P] and [Q].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CGroups/G.var.
+inline "cic:/CoRN/algebra/CGroups/G.var".
 
-inline cic:/CoRN/algebra/CGroups/F.var.
+inline "cic:/CoRN/algebra/CGroups/F.var".
 
-inline cic:/CoRN/algebra/CGroups/F'.var.
+inline "cic:/CoRN/algebra/CGroups/F'.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/algebra/CGroups/P.con.
+inline "cic:/CoRN/algebra/CGroups/P.con".
 
-inline cic:/CoRN/algebra/CGroups/Q.con.
+inline "cic:/CoRN/algebra/CGroups/Q.con".
 
 (* end hide *)
 
@@ -330,9 +340,9 @@ inline cic:/CoRN/algebra/CGroups/Q.con.
 Section Part_Function_Inv.
 *)
 
-inline cic:/CoRN/algebra/CGroups/part_function_inv_strext.con.
+inline "cic:/CoRN/algebra/CGroups/part_function_inv_strext.con".
 
-inline cic:/CoRN/algebra/CGroups/Finv.con.
+inline "cic:/CoRN/algebra/CGroups/Finv.con".
 
 (* UNEXPORTED
 End Part_Function_Inv.
@@ -342,9 +352,9 @@ End Part_Function_Inv.
 Section Part_Function_Minus.
 *)
 
-inline cic:/CoRN/algebra/CGroups/part_function_minus_strext.con.
+inline "cic:/CoRN/algebra/CGroups/part_function_minus_strext.con".
 
-inline cic:/CoRN/algebra/CGroups/Fminus.con.
+inline "cic:/CoRN/algebra/CGroups/Fminus.con".
 
 (* UNEXPORTED
 End Part_Function_Minus.
@@ -355,17 +365,17 @@ End Part_Function_Minus.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CGroups/R.var.
+inline "cic:/CoRN/algebra/CGroups/R.var".
 
-inline cic:/CoRN/algebra/CGroups/included_FInv.con.
+inline "cic:/CoRN/algebra/CGroups/included_FInv.con".
 
-inline cic:/CoRN/algebra/CGroups/included_FInv'.con.
+inline "cic:/CoRN/algebra/CGroups/included_FInv'.con".
 
-inline cic:/CoRN/algebra/CGroups/included_FMinus.con.
+inline "cic:/CoRN/algebra/CGroups/included_FMinus.con".
 
-inline cic:/CoRN/algebra/CGroups/included_FMinus'.con.
+inline "cic:/CoRN/algebra/CGroups/included_FMinus'.con".
 
-inline cic:/CoRN/algebra/CGroups/included_FMinus''.con.
+inline "cic:/CoRN/algebra/CGroups/included_FMinus''.con".
 
 (* UNEXPORTED
 End CGroup_Ops.
@@ -375,10 +385,18 @@ End CGroup_Ops.
 Implicit Arguments Finv [G].
 *)
 
+(* NOTATION
+Notation "{--} x" := (Finv x) (at level 2, right associativity).
+*)
+
 (* UNEXPORTED
 Implicit Arguments Fminus [G].
 *)
 
+(* NOTATION
+Infix "{-}" := Fminus (at level 50, left associativity).
+*)
+
 (* UNEXPORTED
 Hint Resolve included_FInv included_FMinus : included.
 *)