7 kyu

Confusing syntax

30 of 55mhimmel

Description:

In this kata, you will show that there exist unique natural numbers nn and mm such that mnm \leq n... wait, what?

theorem exists_unique_le : ∃! n m : ℕ, m ≤ n :=
sorry
Theorem exists_unique_le : exists! n m : nat, m <= n.
Proof. Admitted.
Theorem Proving
Fundamentals

More By Author:

Check out these other kata created by mhimmel

Stats:

CreatedJul 30, 2020
PublishedJul 30, 2020
Warriors Trained147
Total Skips10
Total Code Submissions91
Total Times Completed55
Lean Completions30
Coq Completions28
Total Stars1
% of votes with a positive feedback rating96% of 14
Total "Very Satisfied" Votes13
Total "Somewhat Satisfied" Votes1
Total "Not Satisfied" Votes0
Total Rank Assessments4
Average Assessed Rank
7 kyu
Highest Assessed Rank
7 kyu
Lowest Assessed Rank
7 kyu
Ad
Contributors
  • mhimmel Avatar
  • Madjosz Avatar
  • monadius Avatar
Ad