proposition: Theorem transfinite_principle r (p:property) (E:= substrate r): worder r -> (forall x, inc x E -> (forall y, inc y E -> glt r y x -> p y) -> p x) -> forall x, inc x E -> p x.
proof: Proof. move => wor hyp x xsr. have or: order r by case: wor. set (s:= Zo (segments r)(fun z => forall y, inc y z -> p y)). have alseg: forall x, inc x s -> segmentp r x. by move=> t /Zo_P [] /(inc_segmentsP wor). have su:forall s', sub s' s -> inc (union s') s. move=> s' s's; apply /Zo_P; split. apply /(inc_segmentsP wor);apply: setU_segment. by move=> t ts'; apply: alseg; apply: s's. move=> y yu; move: (setU_hi yu)=> [v yv vs]. by move: (s's _ vs) => /Zo_hi; apply. have seg: forall x, inc x (substrate r) -> inc (segment r x) s -> inc (segmentc r x) s. move=> y ysr yxs; rewrite /s; apply: Zo_i. apply /(inc_segmentsP wor); apply: (segmentc_segment _ or). move: yxs => /Zo_P [p1 p2]. move=> z; rewrite - segmentc_pr //; case /setU1_P; first by apply: p2. by move=> ->; apply: hyp =>// t _ /segmentP ty; apply: p2. exact: (Zo_hi (transfinite_principle2 wor su seg)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)