Commit 2024-03-20 22:37 c63c49a4
View on Github →chore: golf two_lt_card_iff (#11541)
Makes the proof of this lemma shorter and perhaps cleaner by adding a new lemma and moving it forward to take advantage of the preexisting card_eq_three
chore: golf two_lt_card_iff (#11541)
Makes the proof of this lemma shorter and perhaps cleaner by adding a new lemma and moving it forward to take advantage of the preexisting card_eq_three