letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
intro j; cases (Hxy j); cases H7; cases H8; split; [apply (H9 0);|apply (H11 0)]
letin Ai ≝ (⌊n,≪a n, H1 n≫⌋);
apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); [4: assumption;|2:apply H3;|3:apply H5]
intro j; cases (Hxy j); cases H7; cases H8; split; [apply (H9 0);|apply (H11 0)]