proposition: Theorem finite_increasing_stationary r: order r -> finite_set (substrate r) -> (forall f, increasing_sequence f r -> stationary_sequence f).
proof: Proof. move=> or fs; apply /(increasing_stationaryP or). move=> X Xsr neX; move: (iorder_osr or Xsr) => [pa pb]. apply: finite_set_maximal => //; rewrite pb => //. apply: (sub_finite_set Xsr fs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)