;auto fixed

[helm.git] / helm / software / matita / contribs / RELATIONAL / NLE / props.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
index b571dfc6b46f9e8ab9385bef2462baf354e1d286..549eae418c2762cca71c10f6e8de7a706ba87719 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
@@ -24,7 +24,7 @@ qed.
 theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q.
  unfold NLE.
  intros. decompose.
- apply ex_intro; auto. (**)
+ apply ex_intro; [|auto] (**)
 qed.
 
 theorem nle_refl: \forall x. x <= x.