proposition: Lemma inductive_example1 A F: sub A (\Po F) -> (forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) -> inc (union S) A) -> inductive (sub_order A).
proof: Proof. move=> Ap ih X Xs [oX tX];exists (union X). have [oi si ] := (sub_osr A). move: tX; rewrite iorder_sr// => tX;rewrite si in Xs. have uA: inc (union X) A. by apply: ih; move=> x y xX yX; move: (tX _ _ xX yX); case =>h; move: (iorder_gle1 h) => /sub_gleP [_ _ h1]; [left | right]. split; first by rewrite si. by move=> y yX; apply /sub_gleP;split; [apply: Xs | exact | apply: setU_s1]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)