diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NMulOrder.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMulOrder.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index 804d1ccc0..1d6e8ba0a 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -74,5 +74,9 @@ assert (H3 : 1 < n * m) by now apply (lt_1_l m). rewrite H in H3; false_hyp H3 lt_irrefl. Qed. +(** Alternative name : *) + +Definition mul_eq_1 := eq_mul_1. + End NMulOrderProp. |