diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZDiv.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 3b9720f32..fe66d88c6 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -160,12 +160,12 @@ Qed. Lemma div_1_l: forall a, 1<a -> 1/a == 0. Proof. -intros; apply div_small; split; auto. apply le_succ_diag_r. +intros; apply div_small; split; auto. apply le_0_1. Qed. Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1. Proof. -intros; apply mod_small; split; auto. apply le_succ_diag_r. +intros; apply mod_small; split; auto. apply le_0_1. Qed. Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a. |