proposition: Lemma filternat_and : isfilter_and filternat.
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA