proposition: Lemma leq_af : almost_full le.
proof: Proof. assert (almost_full (fun x y => ~ y < x)). { apply af_from_wf. apply lt_wf. unfold dec_rel. intros. destruct (le_lt_dec x y). left; lia. right; assumption. } apply (af_strengthen H). intros. lia. Defined.
imports: Coq(Arith Wf_nat Lia) AlmostFull.PropBounded(AlmostFull)