From 7de49ed6d5606e958fb00ec48bef43877dd2039a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 16 Mar 2009 12:40:32 +0000 Subject: [PATCH] Adapted to new applyS. --- helm/software/matita/library/nat/gcd.ma | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index 3771bb6e5..b970fb0c3 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/matita/library/nat/gcd.ma @@ -761,10 +761,6 @@ cut (n \divides p \lor n \ndivides p) rewrite > (sym_times q (a1*p)). rewrite > (assoc_times a1). elim H1. - (* - rewrite > H6. - applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2)) - reflexivity. *); applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). (* rewrite < (sym_times n).rewrite < assoc_times. @@ -780,11 +776,14 @@ cut (n \divides p \lor n \ndivides p) rewrite > (sym_times q (a1*p)). rewrite > (assoc_times a1). elim H1.rewrite > H6. + applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). + (* rewrite < sym_times.rewrite > assoc_times. rewrite < (assoc_times q). rewrite < (sym_times n). rewrite < distr_times_minus. apply (witness ? ? (n1*a1-q*a)).reflexivity + *) ](* end second case *) |rewrite < (prime_to_gcd_SO n p) [apply eq_minus_gcd|assumption|assumption @@ -882,14 +881,14 @@ cut (n \divides p \lor n \ndivides p) rewrite > distr_times_minus. rewrite > (sym_times p (a1*m)). rewrite > (assoc_times a1). - elim H2. + elim H2.rewrite > H7. applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). |(* second case *) rewrite > (times_n_SO p).rewrite < H6. rewrite > distr_times_minus. rewrite > (sym_times p (a1*m)). rewrite > (assoc_times a1). - elim H2. + elim H2.rewrite > H7. applyS (witness n ? ? (refl_eq ? ?)). ](* end second case *) |rewrite < H1.apply eq_minus_gcd. -- 2.39.2