Skip to content

Commit

Permalink
testing
Browse files Browse the repository at this point in the history
Signed-off-by: Gerwin Klein <[email protected]>
  • Loading branch information
lsf37 committed Jul 9, 2024
1 parent 14eecae commit 7acd391
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion lib/Lib.thy
Original file line number Diff line number Diff line change
Expand Up @@ -2639,6 +2639,6 @@ definition

lemma mod_le_nat:
"x \<le> y \<Longrightarrow> x mod n \<le> y" for y::nat
using mod_less_eq_dividend order_trans by blast
sorry

Check failure on line 2642 in lib/Lib.thy

View workflow job for this annotation

GitHub Actions / File annotations for theory linter

Unfinished proof

This command indicates an unfinished or aborted proof.

end

0 comments on commit 7acd391

Please sign in to comment.