Some lemmas moves to the file they belong to.

[helm.git] / matita / library / assembly / exadecimal.ma

diff --git a/matita/library/assembly/exadecimal.ma b/matita/library/assembly/exadecimal.ma
index 761c06c94718ce89014d63e06622198fad0d83ab..c059b43fa5fe91f079ff05b951157eb6559a9bb8 100644 (file)
--- a/matita/library/assembly/exadecimal.ma
+++ b/matita/library/assembly/exadecimal.ma
@@ -768,8 +768,7 @@ lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
  elim b;
  simplify;
  [
- |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
-   repeat (apply lt_S_S)
+ |*: repeat (apply lt_to_lt_S_S)
  ];
  autobatch.
 qed.