From af329cf0e0db4521e5f3d333802928e1425e9f75 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 30 Oct 2006 16:56:28 +0000 Subject: [PATCH] library = yes! --- helm/software/matita/library/nat/ord.ma | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index 1ec8f68c5..ba08a0dcf 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -168,7 +168,7 @@ apply p_ord_exp apply le_times_l. assumption. apply le_times_r.assumption. - alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con". +alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con". apply not_eq_to_le_to_lt. unfold.intro.apply H1. rewrite < H3. @@ -213,9 +213,9 @@ unfold.intro. elim (divides_times_to_divides ? ? ? H H9). apply (absurd ? ? H10 H5). apply (absurd ? ? H10 H7). -rewrite > H6. -rewrite > H8. -auto paramodulation. +(* rewrite > H6. +rewrite > H8. *) +auto paramodulation library=yes. unfold prime in H. elim H. assumption. qed. -- 2.39.2