Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / model / structures / Qsec.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qsec.mma b/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qsec.mma
index 2a023a171377e01df7f5345358666562dd6d70bf..396411708559824085ebf310ba0fd3b039864138 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qsec.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/structures/Qsec.mma
@@ -50,23 +50,23 @@ Section Q
 
 inline procedural "cic:/CoRN/model/structures/Qsec/Q.ind".
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qeq.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qeq.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qap.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qap.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qopp.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qopp.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/QZERO.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/QZERO.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/QONE.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/QONE.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qinv.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qinv.con" as definition.
 
 (* UNEXPORTED
 End Q
@@ -99,168 +99,168 @@ Notation "{-Q}" := Qopp (at level 1, left associativity).
 (*#* ***Constants
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/QTWO.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/QTWO.con" as definition.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/QFOUR.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/QFOUR.con" as definition.
 
 (*#* ***Equality
 Here we prove that [QONE] is #<i>#%\emph{%not equal%}%#</i># to [QZERO]: 
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/ONEQ_neq_ZEROQ.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/ONEQ_neq_ZEROQ.con" as theorem.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/refl_Qeq.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/refl_Qeq.con" as theorem.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/sym_Qeq.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/sym_Qeq.con" as theorem.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/trans_Qeq.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/trans_Qeq.con" as theorem.
 
 (*#*
  The equality is decidable: 
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/dec_Qeq.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/dec_Qeq.con" as theorem.
 
 (*#* ***Apartness
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Q_non_zero.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Q_non_zero.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_irreflexive0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_irreflexive0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_symmetric0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_symmetric0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_cotransitive0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_cotransitive0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_tight0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_tight0.con" as lemma.
 
 (*#* ***Addition
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_simpl.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_simpl.con" as theorem.
 
 (*#* 
  Addition is associative:
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_assoc.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_assoc.con" as theorem.
 
 (*#*
  [QZERO] as the neutral element for addition:
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/QZERO_right.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/QZERO_right.con" as theorem.
 
 (*#*
  Commutativity of addition:
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_sym.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_sym.con" as theorem.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_strext0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_strext0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/ZEROQ_as_rht_unit0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/ZEROQ_as_rht_unit0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/ZEROQ_as_lft_unit0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/ZEROQ_as_lft_unit0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_is_commut0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_is_commut0.con" as lemma.
 
 (*#* ***Opposite
  [{-Q}] is a well defined unary operation: 
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qopp_simpl.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qopp_simpl.con" as lemma.
 
 (*#*
  The group equation for [{-Q}]
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_inverse_r.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_inverse_r.con" as theorem.
 
 (*#* ***Multiplication
 Next we shall prove the properties of multiplication. First we prove
 that [{*Q}] is well-defined
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_simpl.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_simpl.con" as theorem.
 
 (*#*
  and it is associative:
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_assoc.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_assoc.con" as theorem.
 
 (*#*
  [QONE] is the neutral element for multiplication:
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_n_1.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_n_1.con" as theorem.
 
 (*#*
  The commutativity for [{*Q}]:
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_sym.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_sym.con" as theorem.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_plus_distr_r.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_plus_distr_r.con" as theorem.
 
 (*#*
  And a property of multiplication which says if [x [~=] Zero] and [xy [=] Zero] then [y [=] Zero]:
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_eq.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_eq.con" as theorem.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_strext0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_strext0.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/nonZero.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/nonZero.con" as lemma.
 
 (*#* ***Inverse
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qinv_strext.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qinv_strext.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qinv_is_inv.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qinv_is_inv.con" as lemma.
 
 (*#* ***Less-than
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_wd_right.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_wd_right.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_wd_left.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_wd_left.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_eq_gt_dec.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_eq_gt_dec.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_transitive_unfolded.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_transitive_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_strext_unfolded.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_strext_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_irreflexive_unfolded.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_irreflexive_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_antisymmetric_unfolded.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_antisymmetric_unfolded.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_resp_Qlt.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_resp_Qlt.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_resp_pos_Qlt.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_resp_pos_Qlt.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_gives_apartness.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_gives_apartness.con" as lemma.
 
 (*#* ***Miscellaneous
 We consider the injection [inject_Z] from [Z] to [Q] as a coercion.
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/inject_Z.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/inject_Z.con" as definition.
 
 (* COERCION
 cic:/matita/CoRN-Procedural/model/structures/Qsec/inject_Z.con
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/injz_plus.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/injz_plus.con" as lemma.
 
-inline procedural "cic:/CoRN/model/structures/Qsec/injZ_One.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/injZ_One.con" as lemma.
 
 (*#* We can always find a natural number that is bigger than a given rational
 number.
 *)
 
-inline procedural "cic:/CoRN/model/structures/Qsec/Q_is_archemaedian0.con".
+inline procedural "cic:/CoRN/model/structures/Qsec/Q_is_archemaedian0.con" as theorem.