matita/matita/contribs/procedural/CoRN/algebra/CLogic.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: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *)
  20
  21 (*#* printing Not %\ensuremath\neg% #~# *)
  22
  23 (*#* printing CNot %\ensuremath\neg% #~# *)
  24
  25 (*#* printing Iff %\ensuremath\Leftrightarrow% #&hArr;# *)
  26
  27 (*#* printing CFalse %\ensuremath\bot% #&perp;# *)
  28
  29 (*#* printing False %\ensuremath\bot% #&perp;# *)
  30
  31 (*#* printing CTrue %\ensuremath\top% *)
  32
  33 (*#* printing True %\ensuremath\top% *)
  34
  35 (*#* printing or %\ensuremath{\mathrel\vee}% *)
  36
  37 (*#* printing and %\ensuremath{\mathrel\wedge}% *)
  38
  39 include "algebra/Basics.ma".
  40
  41 (*#* *Extending the Coq Logic
  42 Because notions of apartness and order have computational meaning, we
  43 will have to define logical connectives in [Type].  In order to
  44 keep a syntactic distinction between types of terms, we define [CProp]
  45 as an alias for [Type], to be used as type of (computationally meaningful)
  46 propositions.
  47
  48 Falsehood and negation will typically not be needed in [CProp], as
  49 they are used to refer to negative statements, which carry no
  50 computational meaning.  Therefore, we will simply define a negation
  51 operator from [Type] to [Prop] .
  52
  53 Conjunction, disjunction and existential quantification will have to come in
  54 multiple varieties.  For conjunction, we will need four operators of type
  55 [s1->s2->s3], where [s3] is [Prop] if both [s1] and [s2]
  56 are [Prop] and [CProp] otherwise.
  57 We here take advantage of the inclusion of [Prop] in [Type].
  58
  59 Disjunction is slightly different, as it will always return a value in [CProp] even
  60 if both arguments are propositions.  This is because in general
  61 it may be computationally important to know which of the two branches of the
  62 disjunction actually holds.
  63
  64 Existential quantification will similarly always return a value in [CProp].
  65
  66 - [CProp]-valued conjuction will be denoted as [and];
  67 - [Crop]-valued conjuction will be denoted as [or];
  68 - Existential quantification will be written as [{x:A & B}] or [{x:A | B}],
  69 according to whether [B] is respectively of type [CProp] or [Prop].
  70
  71 In a few specific situations we do need truth, false and negation in [CProp],
  72 so we will also introduce them; this should be a temporary option.
  73
  74 Finally, for other formulae that might occur in our [CProp]-valued
  75 propositions, such as [(le m n)], we have to introduce a [CProp]-valued
  76 version.
  77 *)
  78
  79 inline procedural "cic:/CoRN/algebra/CLogic/CProp.con" as definition.
  80
  81 (* UNEXPORTED
  82 Section Basics
  83 *)
  84
  85 (*#* ** Basics
  86 Here we treat conversion from [Prop] to [CProp] and vice versa,
  87 and some basic connectives in [CProp].
  88 *)
  89
  90 inline procedural "cic:/CoRN/algebra/CLogic/Not.con" as definition.
  91
  92 inline procedural "cic:/CoRN/algebra/CLogic/CAnd.ind".
  93
  94 inline procedural "cic:/CoRN/algebra/CLogic/Iff.con" as definition.
  95
  96 inline procedural "cic:/CoRN/algebra/CLogic/CFalse.ind".
  97
  98 inline procedural "cic:/CoRN/algebra/CLogic/CTrue.ind".
  99
 100 inline procedural "cic:/CoRN/algebra/CLogic/proj1_sigT.con" as definition.
 101
 102 inline procedural "cic:/CoRN/algebra/CLogic/proj2_sigT.con" as definition.
 103
 104 inline procedural "cic:/CoRN/algebra/CLogic/sig2T.ind".
 105
 106 inline procedural "cic:/CoRN/algebra/CLogic/proj1_sig2T.con" as definition.
 107
 108 inline procedural "cic:/CoRN/algebra/CLogic/proj2a_sig2T.con" as definition.
 109
 110 inline procedural "cic:/CoRN/algebra/CLogic/proj2b_sig2T.con" as definition.
 111
 112 inline procedural "cic:/CoRN/algebra/CLogic/toCProp.ind".
 113
 114 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_e.con" as lemma.
 115
 116 inline procedural "cic:/CoRN/algebra/CLogic/CNot.con" as definition.
 117
 118 inline procedural "cic:/CoRN/algebra/CLogic/Ccontrapos'.con" as lemma.
 119
 120 inline procedural "cic:/CoRN/algebra/CLogic/COr.ind".
 121
 122 (*#*
 123 Some lemmas to make it possible to use [Step] when reasoning with
 124 biimplications.*)
 125
 126 (* NOTATION
 127 Infix "IFF" := Iff (at level 60, right associativity).
 128 *)
 129
 130 inline procedural "cic:/CoRN/algebra/CLogic/Iff_left.con" as lemma.
 131
 132 inline procedural "cic:/CoRN/algebra/CLogic/Iff_right.con" as lemma.
 133
 134 inline procedural "cic:/CoRN/algebra/CLogic/Iff_refl.con" as lemma.
 135
 136 inline procedural "cic:/CoRN/algebra/CLogic/Iff_sym.con" as lemma.
 137
 138 inline procedural "cic:/CoRN/algebra/CLogic/Iff_trans.con" as lemma.
 139
 140 inline procedural "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con" as lemma.
 141
 142 (* UNEXPORTED
 143 Declare Right Step Iff_right.
 144 *)
 145
 146 (* UNEXPORTED
 147 Declare Left Step Iff_left.
 148 *)
 149
 150 (* UNEXPORTED
 151 Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra.
 152 *)
 153
 154 (* UNEXPORTED
 155 End Basics
 156 *)
 157
 158 (* begin hide *)
 159
 160 (* NOTATION
 161 Infix "or" := COr (at level 85, right associativity).
 162 *)
 163
 164 (* NOTATION
 165 Infix "and" := CAnd (at level 80, right associativity).
 166 *)
 167
 168 (* end hide *)
 169
 170 inline procedural "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con" as lemma.
 171
 172 inline procedural "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con" as lemma.
 173
 174 (* begin hide *)
 175
 176 (* NOTATION
 177 Notation "{ x : A  |  P }" := (sigT (fun x : A => P):CProp)
 178   (at level 0, x at level 99) : type_scope.
 179 *)
 180
 181 (* NOTATION
 182 Notation "{ x : A  |  P  |  Q }" :=
 183   (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
 184   type_scope.
 185 *)
 186
 187 (* end hide *)
 188
 189 (*
 190 Section test.
 191
 192 Variable A:Type.
 193 Variables P,Q:A->Prop.
 194 Variables X,Y:A->CProp.
 195
 196 Check {x:A | (P x)}.
 197 Check {x:A |(X x)}.
 198 Check {x:A | (X x) | (Y x)}.
 199 Check {x:A | (P x) | (Q x)}.
 200 Check {x:A | (P x) | (X x)}.
 201 Check {x:A | (X x) | (P x)}.
 202
 203 End test.
 204 *)
 205
 206 (* UNEXPORTED
 207 Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core.
 208 *)
 209
 210 (* UNEXPORTED
 211 Section Choice
 212 *)
 213
 214 (* **Choice
 215 Let [P] be a predicate on $\NN^2$#N times N#.
 216 *)
 217
 218 (* UNEXPORTED
 219 cic:/CoRN/algebra/CLogic/Choice/P.var
 220 *)
 221
 222 inline procedural "cic:/CoRN/algebra/CLogic/choice.con" as lemma.
 223
 224 (* UNEXPORTED
 225 End Choice
 226 *)
 227
 228 (* UNEXPORTED
 229 Section Logical_Remarks
 230 *)
 231
 232 (*#* We prove a few logical results which are helpful to have as lemmas
 233 when [A], [B] and [C] are non trivial.
 234 *)
 235
 236 inline procedural "cic:/CoRN/algebra/CLogic/CNot_Not_or.con" as lemma.
 237
 238 inline procedural "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con" as lemma.
 239
 240 (* UNEXPORTED
 241 End Logical_Remarks
 242 *)
 243
 244 (* UNEXPORTED
 245 Section CRelation_Definition
 246 *)
 247
 248 (*#* ** [CProp]-valued Relations
 249 Similar to Relations.v in Coq's standard library.
 250
 251 %\begin{convention}% Let [A:Type] and [R:Crelation].
 252 %\end{convention}%
 253 *)
 254
 255 (* UNEXPORTED
 256 cic:/CoRN/algebra/CLogic/CRelation_Definition/A.var
 257 *)
 258
 259 inline procedural "cic:/CoRN/algebra/CLogic/Crelation.con" as definition.
 260
 261 (* UNEXPORTED
 262 cic:/CoRN/algebra/CLogic/CRelation_Definition/R.var
 263 *)
 264
 265 inline procedural "cic:/CoRN/algebra/CLogic/Creflexive.con" as definition.
 266
 267 inline procedural "cic:/CoRN/algebra/CLogic/Ctransitive.con" as definition.
 268
 269 inline procedural "cic:/CoRN/algebra/CLogic/Csymmetric.con" as definition.
 270
 271 inline procedural "cic:/CoRN/algebra/CLogic/Cequiv.con" as definition.
 272
 273 (* UNEXPORTED
 274 End CRelation_Definition
 275 *)
 276
 277 (* UNEXPORTED
 278 Section TRelation_Definition
 279 *)
 280
 281 (*#* ** [Prop]-valued Relations
 282 Analogous.
 283
 284 %\begin{convention}% Let [A:Type] and [R:Trelation].
 285 %\end{convention}%
 286 *)
 287
 288 (* UNEXPORTED
 289 cic:/CoRN/algebra/CLogic/TRelation_Definition/A.var
 290 *)
 291
 292 inline procedural "cic:/CoRN/algebra/CLogic/Trelation.con" as definition.
 293
 294 (* UNEXPORTED
 295 cic:/CoRN/algebra/CLogic/TRelation_Definition/R.var
 296 *)
 297
 298 inline procedural "cic:/CoRN/algebra/CLogic/Treflexive.con" as definition.
 299
 300 inline procedural "cic:/CoRN/algebra/CLogic/Ttransitive.con" as definition.
 301
 302 inline procedural "cic:/CoRN/algebra/CLogic/Tsymmetric.con" as definition.
 303
 304 inline procedural "cic:/CoRN/algebra/CLogic/Tequiv.con" as definition.
 305
 306 (* UNEXPORTED
 307 End TRelation_Definition
 308 *)
 309
 310 inline procedural "cic:/CoRN/algebra/CLogic/eqs.ind".
 311
 312 (* UNEXPORTED
 313 Section le_odd
 314 *)
 315
 316 (*#* ** The relation [le], [lt], [odd] and [even] in [CProp]
 317 *)
 318
 319 inline procedural "cic:/CoRN/algebra/CLogic/Cle.ind".
 320
 321 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con" as theorem.
 322
 323 inline procedural "cic:/CoRN/algebra/CLogic/my_Cle_ind.con" as theorem.
 324
 325 inline procedural "cic:/CoRN/algebra/CLogic/Cle_n_S.con" as theorem.
 326
 327 inline procedural "cic:/CoRN/algebra/CLogic/toCle.con" as lemma.
 328
 329 (* UNEXPORTED
 330 Hint Resolve toCle.
 331 *)
 332
 333 inline procedural "cic:/CoRN/algebra/CLogic/Cle_to.con" as lemma.
 334
 335 inline procedural "cic:/CoRN/algebra/CLogic/Clt.con" as definition.
 336
 337 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_lt.con" as lemma.
 338
 339 inline procedural "cic:/CoRN/algebra/CLogic/Clt_to.con" as lemma.
 340
 341 inline procedural "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con" as lemma.
 342
 343 inline procedural "cic:/CoRN/algebra/CLogic/Cnat_total_order.con" as lemma.
 344
 345 inline procedural "cic:/CoRN/algebra/CLogic/Codd.ind".
 346
 347 inline procedural "cic:/CoRN/algebra/CLogic/Codd_even_to.con" as lemma.
 348
 349 inline procedural "cic:/CoRN/algebra/CLogic/Codd_to.con" as lemma.
 350
 351 inline procedural "cic:/CoRN/algebra/CLogic/Ceven_to.con" as lemma.
 352
 353 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd_even.con" as lemma.
 354
 355 inline procedural "cic:/CoRN/algebra/CLogic/to_Codd.con" as lemma.
 356
 357 inline procedural "cic:/CoRN/algebra/CLogic/to_Ceven.con" as lemma.
 358
 359 (* UNEXPORTED
 360 End le_odd
 361 *)
 362
 363 (* UNEXPORTED
 364 Section Misc
 365 *)
 366
 367 (*#* **Miscellaneous
 368 *)
 369
 370 inline procedural "cic:/CoRN/algebra/CLogic/CZ_exh.con" as lemma.
 371
 372 inline procedural "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con" as lemma.
 373
 374 inline procedural "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con" as lemma.
 375
 376 inline procedural "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con" as lemma.
 377
 378 inline procedural "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con" as lemma.
 379
 380 inline procedural "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con" as lemma.
 381
 382 (* UNEXPORTED
 383 End Misc
 384 *)
 385
 386 (*#* **Results about the natural numbers
 387
 388 We now define a class of predicates on a finite subset of natural
 389 numbers that will be important throughout all our work.  Essentially,
 390 these are simply setoid predicates, but for clarity we will never
 391 write them in that form but we will single out the preservation of the
 392 setoid equality.
 393 *)
 394
 395 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con" as definition.
 396
 397 inline procedural "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con" as definition.
 398
 399 (* UNEXPORTED
 400 Implicit Arguments nat_less_n_pred [n].
 401 *)
 402
 403 (* UNEXPORTED
 404 Implicit Arguments nat_less_n_pred' [n].
 405 *)
 406
 407 (* UNEXPORTED
 408 Section Odd_and_Even
 409 *)
 410
 411 (*#*
 412 For our work we will many times need to distinguish cases between even or odd numbers.
 413 We begin by proving that this case distinction is decidable.
 414 Next, we prove the usual results about sums of even and odd numbers:
 415 *)
 416
 417 inline procedural "cic:/CoRN/algebra/CLogic/even_plus_n_n.con" as lemma.
 418
 419 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con" as lemma.
 420
 421 (*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
 422 *)
 423
 424 inline procedural "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con" as lemma.
 425
 426 (* UNEXPORTED
 427 End Odd_and_Even
 428 *)
 429
 430 (* UNEXPORTED
 431 Hint Resolve even_plus_n_n: arith.
 432 *)
 433
 434 (* UNEXPORTED
 435 Hint Resolve toCle: core.
 436 *)
 437
 438 (* UNEXPORTED
 439 Section Natural_Numbers
 440 *)
 441
 442 (*#* **Algebraic Properties
 443
 444 We now present a series of trivial things proved with [Omega] that are
 445 stated as lemmas to make proofs shorter and to aid in auxiliary
 446 definitions.  Giving a name to these results allows us to use them in
 447 definitions keeping conciseness.
 448 *)
 449
 450 inline procedural "cic:/CoRN/algebra/CLogic/Clt_le_weak.con" as lemma.
 451
 452 inline procedural "cic:/CoRN/algebra/CLogic/lt_5.con" as lemma.
 453
 454 inline procedural "cic:/CoRN/algebra/CLogic/lt_8.con" as lemma.
 455
 456 inline procedural "cic:/CoRN/algebra/CLogic/pred_lt.con" as lemma.
 457
 458 inline procedural "cic:/CoRN/algebra/CLogic/lt_10.con" as lemma.
 459
 460 inline procedural "cic:/CoRN/algebra/CLogic/lt_pred'.con" as lemma.
 461
 462 inline procedural "cic:/CoRN/algebra/CLogic/le_1.con" as lemma.
 463
 464 inline procedural "cic:/CoRN/algebra/CLogic/le_2.con" as lemma.
 465
 466 inline procedural "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con" as lemma.
 467
 468 inline procedural "cic:/CoRN/algebra/CLogic/not_not_lt.con" as lemma.
 469
 470 inline procedural "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con" as lemma.
 471
 472 (*#* We now prove some properties of functions on the natural numbers.
 473
 474 %\begin{convention}% Let [H:nat->nat].
 475 %\end{convention}%
 476 *)
 477
 478 (* UNEXPORTED
 479 cic:/CoRN/algebra/CLogic/Natural_Numbers/h.var
 480 *)
 481
 482 (*#*
 483 First we characterize monotonicity by a local condition: if [h(n) < h(n+1)]
 484 for every natural number [n] then [h] is monotonous.  An analogous result
 485 holds for weak monotonicity.
 486 *)
 487
 488 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con" as lemma.
 489
 490 inline procedural "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con" as lemma.
 491
 492 (*#* A strictly increasing function is injective: *)
 493
 494 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con" as lemma.
 495
 496 (*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
 497
 498 inline procedural "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con" as lemma.
 499
 500 (*#*
 501 The last lemmas in this section state that a monotonous function in the
 502  natural numbers completely covers the natural numbers, that is, for every
 503 natural number [n] there is an [i] such that [h(i) <= n<(n+1) <= h(i+1)].
 504 These are useful for integration.
 505 *)
 506
 507 inline procedural "cic:/CoRN/algebra/CLogic/mon_fun_covers.con" as lemma.
 508
 509 inline procedural "cic:/CoRN/algebra/CLogic/weird_mon_covers.con" as lemma.
 510
 511 (* UNEXPORTED
 512 End Natural_Numbers
 513 *)
 514
 515 (*#*
 516 Useful for the Fundamental Theorem of Algebra.
 517 *)
 518
 519 inline procedural "cic:/CoRN/algebra/CLogic/kseq_prop.con" as lemma.
 520
 521 (* UNEXPORTED
 522 Section Predicates_to_CProp
 523 *)
 524
 525 (*#* **Logical Properties
 526
 527 This section contains lemmas that aid in logical reasoning with
 528 natural numbers.  First, we present some principles of induction, both
 529 for [CProp]- and [Prop]-valued predicates.  We begin by presenting the
 530 results for [CProp]-valued predicates:
 531 *)
 532
 533 inline procedural "cic:/CoRN/algebra/CLogic/even_induction.con" as lemma.
 534
 535 inline procedural "cic:/CoRN/algebra/CLogic/odd_induction.con" as lemma.
 536
 537 inline procedural "cic:/CoRN/algebra/CLogic/four_induction.con" as lemma.
 538
 539 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con" as lemma.
 540
 541 inline procedural "cic:/CoRN/algebra/CLogic/odd_double_ind.con" as lemma.
 542
 543 (*#* For subsetoid predicates in the natural numbers we can eliminate
 544 disjunction (and existential quantification) as follows.
 545 *)
 546
 547 inline procedural "cic:/CoRN/algebra/CLogic/finite_or_elim.con" as lemma.
 548
 549 inline procedural "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con" as lemma.
 550
 551 (* UNEXPORTED
 552 End Predicates_to_CProp
 553 *)
 554
 555 (* UNEXPORTED
 556 Section Predicates_to_Prop
 557 *)
 558
 559 (*#* Finally, analogous results for [Prop]-valued predicates are presented for
 560 completeness's sake.
 561 *)
 562
 563 inline procedural "cic:/CoRN/algebra/CLogic/even_ind.con" as lemma.
 564
 565 inline procedural "cic:/CoRN/algebra/CLogic/odd_ind.con" as lemma.
 566
 567 inline procedural "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con" as lemma.
 568
 569 inline procedural "cic:/CoRN/algebra/CLogic/four_ind.con" as lemma.
 570
 571 (* UNEXPORTED
 572 End Predicates_to_Prop
 573 *)
 574
 575 (*#* **Integers
 576
 577 Similar results for integers.
 578 *)
 579
 580 (* begin hide *)
 581
 582 (* UNEXPORTED
 583 Tactic Notation "ElimCompare" constr(c) constr(d) :=  elim_compare c d.
 584 *)
 585
 586 (* end hide *)
 587
 588 inline procedural "cic:/CoRN/algebra/CLogic/Zlts.con" as definition.
 589
 590 inline procedural "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con" as lemma.
 591
 592 inline procedural "cic:/CoRN/algebra/CLogic/CZlt_to.con" as lemma.
 593
 594 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_1.con" as lemma.
 595
 596 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_2.con" as lemma.
 597
 598 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_3.con" as lemma.
 599
 600 (*#* The following have unusual names, in line with the series of lemmata in
 601 fast_integers.v.
 602 *)
 603
 604 inline procedural "cic:/CoRN/algebra/CLogic/ZL4'.con" as lemma.
 605
 606 inline procedural "cic:/CoRN/algebra/CLogic/ZL9.con" as lemma.
 607
 608 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_4.con" as theorem.
 609
 610 inline procedural "cic:/CoRN/algebra/CLogic/Zsgn_5.con" as theorem.
 611
 612 inline procedural "cic:/CoRN/algebra/CLogic/nat_nat_pos.con" as lemma.
 613
 614 inline procedural "cic:/CoRN/algebra/CLogic/S_predn.con" as theorem.
 615
 616 inline procedural "cic:/CoRN/algebra/CLogic/absolu_1.con" as lemma.
 617
 618 inline procedural "cic:/CoRN/algebra/CLogic/absolu_2.con" as lemma.
 619
 620 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con" as lemma.
 621
 622 inline procedural "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con" as lemma.
 623
 624 inline procedural "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con" as lemma.
 625
 626 (* NOTATION
 627 Notation ProjT1 := (proj1_sigT _ _).
 628 *)
 629
 630 (* NOTATION
 631 Notation ProjT2 := (proj2_sigT _ _).
 632 *)
 633