proposition: Lemma ordinal_with_AF x: (forall y, sub y x -> foundation_prop y) -> (ordinalp x <-> ordinal_altp x).
proof: Proof. move => hc; split. move => ox; split; first by apply: (ordinal_transitive ox). move => a b ax bx. exact (ordinal_inA (Os_ordinal ox ax) (Os_ordinal ox bx)). move => [trx xp]. have hb: forall a b c, inc a x -> inc b x -> inc c x -> foundation_prop (tripleton a b c). by move => a b c ax bcx cx; apply:hc => y /set3_P; case; move => ->. have ha: asymmetric_set x. move => u v ux vx uv vu. case: (hb _ _ _ ux ux vx). apply /nonemptyP; exists v; rewrite/tripleton;fprops. rewrite /tripleton -/(singleton _) setU2_11. move => [y /set2_P]; case => ->; apply/nonemptyP. exists v; fprops. exists u; fprops. apply /ordinal_pr1; split => //. have pa: (substrate (ordinal_oa x)) = x. by rewrite graph_on_sr => // a ax; right. have pb: order (ordinal_oa x). pose r a b := [/\ inc a x, inc b x & (inc a b \/ a = b)]. have ->: ((ordinal_oa x) = graph_on r x). by apply: Zo_exten1 => t /setX_P [_ px qx]; split => //; move => [_ _]. apply:order_from_rel; split. move => b a c [ax bx ab] [_ cx bc]; split => //. case :(ab) => ab'; last by ue. case :bc=> bc; last by ue. move: (ha _ _ ax bx ab') => nba. case: (xp _ _ ax cx); first (by left); last first. by move => ac; case: nba; rewrite ac. move => ca. case: (hb _ _ _ ax bx cx). by move/set0_P=> h; case: (h a); apply/set3_P; constructor 1. move => [y /set3_P ya]; move /set0_P => h; case: ya => yv. case: (h c); rewrite yv;apply /setI2_P ; split=> //; apply/set3_P; in_TP4. case: (h a); rewrite yv;apply /setI2_P ; split=> //; apply/set3_P; in_TP4. case: (h b); rewrite yv;apply /setI2_P ; split=> //; apply/set3_P; in_TP4. move => a b [ax bx]; case => // ab [_ _]; case => // ba. case: (ha _ _ ax bx ab ba). by move => a b [ax bx etc]; split; split => //; right. split => //; rewrite pa. move => y yx /nonemptyP ney. case: (hc _ yx) => // [] [z zy ztc]. exists z; red; rewrite (iorder_sr pb); last by ue. split => // t ty; apply /iorder_gle0P => //. move: (yx _ zy)(yx _ ty) => zx tx. apply /graph_on_P1; split => //. case: (xp _ _ zx tx); [ by left | move => tz; empty_tac1 t | by right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)