proposition: Lemma af_finite (k:nat) : almost_full (@eq_fin k).
proof: Proof. set (f1 (x:Finite k) := match x with | @FinIntro _ kx _ => kx end). set (f2 (x:Finite k) := match x with | @FinIntro _ kx _ => k - kx end). assert (almost_full (fun x y => f1 x <= f1 y /\ f2 x <= f2 y)). apply af_intersection. apply af_cofmap. apply leq_af. apply af_cofmap. apply leq_af. unfold almost_full in *. destruct H. exists x. eapply sec_strengthen. 2: apply H. intros; simpl. destruct x0. destruct y. simpl in H0. unfold eq_fin. lia. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)