proposition: Lemma stratified_setrP i (E:= stratified_setr i): ordinalp i -> (forall x, inc x E <-> (W x /\ idx x = i)).
proof: Proof. move => oi. have H1 :=(stratified_setP (OS_succ oi)). move => x; split; first by move/Zo_P => [/H1 []]. move => [sa sb];apply:Zo_i => //; apply/H1; split => //. by rewrite sb; apply:oltS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)