Lemma filternat_and : isfilter_and filternat. Proof. intros A B. apply hinhfun2. intros Na Nb. exists (max (pr1 Na) (pr1 Nb)). intros n Hn. split. + apply (pr2 Na). eapply istransnatleh, Hn. now apply max_le_l. + apply (pr2 Nb). eapply istransnatleh, Hn. now apply max_le_r. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.