proposition: Lemma squeeze_fin f g h : (\near a, f a <= g a <= h a) -> (\near a, f a \is a fin_num) -> (\near a, h a \is a fin_num) -> (\near a, g a \is a fin_num).
proof: Proof. apply: filterS3 => x /andP[fg gh]. rewrite !fin_numElt => /andP[oof _] /andP[_ hoo]. by rewrite (lt_le_trans oof) ?(le_lt_trans gh). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule