proposition: Lemma setP_inductive A F: sub A (\Po F) -> (forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) -> sub S A ->inc (union S) A) -> inductive (sub_order A).
proof: Proof. move=> sp Sp X XA [oX tX]. move: (sub_osr A) => [or1 sr1]. rewrite iorder_sr in tX; fprops; rewrite sr1 in XA. have p1: inc (union X) A. apply: Sp =>// x y xX yX. case: (tX _ _ xX yX). by move/iorder_gle1 => /sub_gleP [_ _ h]; left. by move/iorder_gle1 => /sub_gleP [_ _ h]; right. exists (union X);split; first by ue. by move=> y yX; apply /sub_gleP;split => //;fprops; apply: setU_s1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)