helm/software/matita/dama/ordered_divisible_group.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/ordered_divisible_group/".
  16
  17 include "nat/orders.ma".
  18 include "nat/times.ma".
  19 include "ordered_group.ma".
  20 include "divisible_group.ma".
  21
  22 record todgroup : Type ≝ {
  23   todg_order:> togroup;
  24   todg_division_: dgroup;
  25   todg_with_: dg_carr todg_division_ = og_abelian_group todg_order
  26 }.
  27
  28 lemma todg_division: todgroup → dgroup.
  29 intro G; apply (mk_dgroup G); unfold abelian_group_OF_todgroup;
  30 cases (todg_with_ G); exact (dg_prop (todg_division_ G));
  31 qed.
  32
  33 coercion cic:/matita/ordered_divisible_group/todg_division.con.
  34
  35 lemma pow_lt: ∀G:todgroup.∀x:G.∀n.0 < x → 0 < x + pow ? x n.
  36 intros (G x n H); elim n; [
  37   simplify; apply (lt_rewr ???? (plus_comm ???));
  38   apply (lt_rewr ???x (zero_neutral ??)); assumption]
  39 simplify; apply (lt_transitive ?? (x+(x)\sup(n1))); [assumption]
  40 apply flt_plusl; apply (lt_rewr ???? (plus_comm ???));
  41 apply (lt_rewl ??? (0 + (x \sup n1)) (eq_sym ??? (zero_neutral ??)));
  42 apply (lt_rewl ???? (plus_comm ???));
  43 apply flt_plusl; assumption;
  44 qed.
  45
  46 lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ pow ? x n.
  47 intros (G x n); elim n; simplify; [apply le_reflexive]
  48 apply (le_transitive ???? H1);
  49 apply (le_rewl ??? (0+(x\sup n1)) (zero_neutral ??));
  50 apply fle_plusr; assumption;
  51 qed.
  52
  53 lemma ge_pow: ∀G:todgroup.∀x:G.∀n.0 < pow ? x n → 0 < x.
  54 intros 3; elim n; [
  55   simplify in l; cases (lt_coreflexive ?? l);]
  56 simplify in l;
  57 cut (0+0<x+(x)\sup(n1));[2:
  58   apply (lt_rewl ??? 0 (zero_neutral ??)); assumption].
  59 cases (pippo4 ????? Hcut); [assumption]
  60 apply f; assumption;
  61 qed.
  62
  63 lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
  64 intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
  65 unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
  66 apply (ge_pow ?? (S (S n1))); apply (lt_rewr ???? f); assumption;
  67 qed.
  68
  69 alias num (instance 0) = "natural number".
  70 axiom core1: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.