diff options
Diffstat (limited to 'test-suite/interactive/ParalITP_smallproofs.v')
| -rw-r--r-- | test-suite/interactive/ParalITP_smallproofs.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v index d2e6794c0b..1f4913b49d 100644 --- a/test-suite/interactive/ParalITP_smallproofs.v +++ b/test-suite/interactive/ParalITP_smallproofs.v @@ -140,35 +140,35 @@ Qed. Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0. Proof. intros. - omega. + lia. Qed. Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0. Proof. intros. - omega. + lia. Qed. Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n). Proof. intros. - omega. + lia. Qed. Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0. Proof. - intros; omega. + intros; lia. Qed. Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0. Proof. - intros; omega. + intros; lia. Qed. Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n. Proof. intros. - omega. + lia. Qed. @@ -1414,13 +1414,13 @@ Qed. Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n. Proof. intros. - omega. + lia. Qed. Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n. Proof. intros. - omega. + lia. Qed. @@ -1501,7 +1501,7 @@ Proof. [ replace (Zabs_nat x) with (Zabs_nat (x - 1 + 1)); [ idtac | apply f_equal with Z; auto with zarith ]; rewrite absolu_plus; - [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; omega + [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; lia | auto with zarith | intro; discriminate ] | rewrite <- H1; reflexivity ]. |