set "baseuri" "cic:/matita/CoRN-Decl/model/abgroups/QSposabgroup".
+include "CoRN.ma".
+
(* $Id: QSposabgroup.v,v 1.5 2004/04/08 08:20:31 lcf Exp $ *)
-(* INCLUDE
-QSposgroup
-*)
+include "model/groups/QSposgroup.ma".
-(* INCLUDE
-CAbGroups
-*)
+include "algebra/CAbGroups.ma".
(*#* **Example of an abelian group: $\langle$#⟨#[Qpos],$(x,y) \mapsto xy/2$ #(x,y) ↦ xy/2#$\rangle$#⟩#
The positive rational numbers form with the operation $(x,y) \mapsto xy/2$ #(x,y) ↦ xy/2# an abelian group.
*)
-inline cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_is_CAbGroup.con.
+inline "cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_is_CAbGroup.con".
-inline cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_as_CAbGroup.con.
+inline "cic:/CoRN/model/abgroups/QSposabgroup/Qpos_multdiv2_as_CAbGroup.con".