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. apply (af_strengthen H). intros. destruct H0. destruct x. destruct y. unfold eq_fin. simpl in *. lia. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)