diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NOrder.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 9ddaa9a2f..7b4645be3 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -407,7 +407,7 @@ Variable R : N -> N -> Prop. Hypothesis R_wd : relation_wd Neq Neq R. Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. -Proof R_wd. +Proof. apply R_wd. Qed. Theorem le_ind_rel : (forall m : N, R 0 m) -> |