proposition: Lemma ordinal_pr x: transitive_set x -> ordinal_set x -> ordinalp x.
proof: Proof. move=> tx alo y syx ty nyx. move: (setC_ne (conj syx nyx)) =>[z /setC_P [zx nzy]]; move: (alo _ zx)=> oz. have zy: (sub y z). move=> t ty'; move: (alo _ (syx _ ty'))=> ot. case:(ordinal_inA oz ot) => zt // ;case:nzy; [ by apply: (ty _ ty')| ue]. case: (equal_or_not y z); first by move=> ->. move=> yz; apply: (tx _ zx _ (oz _ zy ty yz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)