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 set "baseuri" "cic:/matita/divisible_group/".
17 include "nat/orders.ma".
20 let rec pow (G : abelian_group) (x : G) (n : nat) on n : G ≝
21 match n with [ O ⇒ 0 | S m ⇒ x + pow ? x m].
23 interpretation "abelian group pow" 'exp x n =
24 (cic:/matita/divisible_group/pow.con _ x n).
26 record dgroup : Type ≝ {
27 dg_carr:> abelian_group;
28 dg_prop: ∀x:dg_carr.∀n:nat.∃y.pow ? y (S n) ≈ x
31 lemma divide: ∀G:dgroup.G → nat → G.
32 intros (G x n); cases (dg_prop G x n); apply w;
35 interpretation "divisible group divide" 'divide x n =
36 (cic:/matita/divisible_group/divide.con _ x n).
39 ∀G:dgroup.∀x:G.∀n. pow ? (x / n) (S n) ≈ x.
40 intro G; cases G; unfold divide; intros (x n); simplify;
41 cases (f x n); simplify; exact H;
44 lemma feq_pow: ∀G:dgroup.∀x,y:G.∀n.x≈y → pow ? x n ≈ pow ? y n.
45 intros (G x y n H); elim n; [apply eq_reflexive]
46 simplify; apply (Eq≈ (x + (pow ? y n1)) H1);
47 apply (Eq≈ (y+pow ? y n1) H (eq_reflexive ??));
50 lemma div1: ∀G:dgroup.∀x:G.x/O ≈ x.
51 intro G; cases G; unfold divide; intros; simplify;
52 cases (f x O); simplify; simplify in H; intro; apply H;
53 apply (ap_rewl ???? (plus_comm ???));
54 apply (ap_rewl ???w (zero_neutral ??)); assumption;