Skip to content

Commit

Permalink
Fix an error (file names in MacOSX)
Browse files Browse the repository at this point in the history
  • Loading branch information
Casteran committed Dec 31, 2023
1 parent 7743965 commit 8bed3a0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Compat_Old_StdLib/SRC/OldArith.v
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Lemma le_add_sub_r (n m:nat) : n <= m -> n + (m - n) = m.
Proof.
intro H; rewrite Nat.add_comm, Nat.sub_add; [ reflexivity | assumption].
Qed.

Lemma sub_add (n m : nat) : n + m - n = m.
Proof.
now rewrite Nat.add_comm, Nat.add_sub.
Expand Down

0 comments on commit 8bed3a0

Please sign in to comment.