proposition: Lemma finite_subsets_order A (I:= Zo (\Po A) finite_set) (r:= sub_order I): [/\ order_on r I, forall x y, inc x I -> inc y I -> inc (x \cup y) I, forall x y, inc x I -> inc y I -> gle r x (x \cup y), forall i, inc i A -> inc (singleton i) I & right_directed r].
proof: Proof. move:(sub_osr I) => pa. have hb: forall x y, inc x I -> inc y I -> inc (x \cup y) I. move => x y /Zo_P [/setP_P xI /card_finite_setP xf] /Zo_P [/setP_P yI /card_finite_setP yf]. apply/Zo_P; split; first by apply/setP_P ;apply:setU2_12S. apply /card_finite_setP. move:(csum2_pr6 x y); rewrite - csum2cl - csum2cr => h. exact:(NS_le_nat h (NS_sum xf yf)). have hc: forall x y, inc x I -> inc y I -> gle r x (x \cup y). move => x y xI yI; apply/sub_gleP; split => //; first by apply: hb. apply: subsetU2l. split => //. - move => i iI; apply/Zo_P; split; first by apply/setP_P => t /set1_P ->. by apply:set1_finite. - move: pa => [or sr];apply/right_directedP; split => // x y xI yI. rewrite sr in xI yI. by exists(x\cup y); split; [ apply: hc | rewrite setU2_C; apply:hc]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)