Commit 370c0cf4 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compatibility with old Coq versions.

parent 2f5854bd
Pipeline #29596 passed with stage
in 10 minutes and 35 seconds
......@@ -154,7 +154,7 @@ Lemma finite_bijective A `{Finite A} B `{Finite B} :
Proof.
split.
- intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
exists f; eauto using finite_inj_surj.
exists f; split; [done|]. by apply finite_inj_surj.
- intros (f&?&?). apply (anti_symm ()); apply finite_inj.
+ by exists f.
+ destruct (surj_cancel f) as (g&?). exists g. apply cancel_inj.
......@@ -274,7 +274,7 @@ Next Obligation.
Qed.
Next Obligation.
intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
eauto using elem_of_enum.
[left|right]; (eexists; split; [done|apply elem_of_enum]).
Qed.
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment