helm/software/matita/contribs/procedural/CoRN/fta/CPoly_Rev.mma

   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 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: CPoly_Rev.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *)
  20
  21 include "algebra/CPoly_Degree.ma".
  22
  23 (*#* * Reverse of polynomials
  24 *)
  25
  26 (* UNEXPORTED
  27 Section Monomials
  28 *)
  29
  30 (*#*
  31 %\begin{convention}% Let [R] be a ring, and let [RX] be the
  32 polynomials over this ring.
  33 %\end{convention}%
  34 *)
  35
  36 (* UNEXPORTED
  37 cic:/CoRN/fta/CPoly_Rev/Monomials/R.var
  38 *)
  39
  40 (* begin hide *)
  41
  42 inline procedural "cic:/CoRN/fta/CPoly_Rev/Monomials/RX.con" "Monomials__" as definition.
  43
  44 (* end hide *)
  45
  46 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom.con" as definition.
  47
  48 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_coeff.con" as lemma.
  49
  50 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_coeff'.con" as lemma.
  51
  52 (* UNEXPORTED
  53 Hint Resolve monom_coeff monom_coeff': algebra.
  54 *)
  55
  56 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_degree.con" as lemma.
  57
  58 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_S.con" as lemma.
  59
  60 (* UNEXPORTED
  61 Hint Resolve monom_S: algebra.
  62 *)
  63
  64 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_wd_lft.con" as lemma.
  65
  66 (* UNEXPORTED
  67 Hint Resolve monom_wd_lft: algebra_c.
  68 *)
  69
  70 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_mult'.con" as lemma.
  71
  72 (* UNEXPORTED
  73 Hint Resolve monom_mult': algebra.
  74 *)
  75
  76 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_mult.con" as lemma.
  77
  78 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_sum.con" as lemma.
  79
  80 (* UNEXPORTED
  81 End Monomials
  82 *)
  83
  84 (* UNEXPORTED
  85 Hint Resolve monom_coeff monom_coeff' monom_mult monom_sum: algebra.
  86 *)
  87
  88 (* UNEXPORTED
  89 Implicit Arguments monom [R].
  90 *)
  91
  92 (* UNEXPORTED
  93 Section Poly_Reverse
  94 *)
  95
  96 (* UNEXPORTED
  97 cic:/CoRN/fta/CPoly_Rev/Poly_Reverse/R.var
  98 *)
  99
 100 (* begin hide *)
 101
 102 inline procedural "cic:/CoRN/fta/CPoly_Rev/Poly_Reverse/RX.con" "Poly_Reverse__" as definition.
 103
 104 (* end hide *)
 105
 106 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev.con" as definition.
 107
 108 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_coeff.con" as lemma.
 109
 110 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_coeff'.con" as lemma.
 111
 112 (* UNEXPORTED
 113 Hint Resolve Rev_coeff Rev_coeff': algebra.
 114 *)
 115
 116 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_wd.con" as lemma.
 117
 118 (* UNEXPORTED
 119 Hint Resolve Rev_wd: algebra_c.
 120 *)
 121
 122 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_rev.con" as lemma.
 123
 124 (* UNEXPORTED
 125 Hint Resolve Rev_rev: algebra.
 126 *)
 127
 128 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_degree_le.con" as lemma.
 129
 130 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_degree.con" as lemma.
 131
 132 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_monom.con" as lemma.
 133
 134 (* UNEXPORTED
 135 Hint Resolve Rev_monom: algebra.
 136 *)
 137
 138 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_zero.con" as lemma.
 139
 140 (* UNEXPORTED
 141 Hint Resolve Rev_zero: algebra.
 142 *)
 143
 144 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_plus.con" as lemma.
 145
 146 (* UNEXPORTED
 147 Hint Resolve Rev_plus: algebra.
 148 *)
 149
 150 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_minus.con" as lemma.
 151
 152 (* UNEXPORTED
 153 Hint Resolve Rev_minus: algebra.
 154 *)
 155
 156 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_sum0.con" as lemma.
 157
 158 (* UNEXPORTED
 159 Hint Resolve Rev_sum0: algebra.
 160 *)
 161
 162 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_sum.con" as lemma.
 163
 164 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_mult.con" as lemma.
 165
 166 (* UNEXPORTED
 167 End Poly_Reverse
 168 *)
 169
 170 (* UNEXPORTED
 171 Hint Resolve Rev_wd: algebra_c.
 172 *)
 173
 174 (* UNEXPORTED
 175 Hint Resolve Rev_rev Rev_mult: algebra.
 176 *)
 177
 178 (* UNEXPORTED
 179 Implicit Arguments Rev [R].
 180 *)
 181