proposition: Lemma minimal_inclusion E y (F:= (\Po E) -s1 emptyset): inc y F -> (minimal (sub_order F) y <-> singletonp y).
proof: Proof. move=> yF. rewrite/minimal (proj2 (sub_osr F)). have Fp x: inc x F <-> (sub x E /\ nonempty x). split. by move/setC1_P => [] /setP_P pa /nonemptyP nw. by move => [pa /nonemptyP pb]; apply/setC1_P; split=> //; apply/setP_P. split. move => [/Fp [yE [z zy]] sp]. have aux: sub (singleton z) y by apply:set1_sub. have stF: inc (singleton z) F. apply /Fp; split; [ apply: sub_trans aux yE | apply: set1_ne]. by exists z; symmetry; apply: sp;apply/graph_on_P1. move=> /singletonP [_ hyp]; split => // x /graph_on_P1 [/Fp [xE [t tx]] _ xy]. apply: extensionality=>//. by move: (xy _ tx)=> ty z zy; rewrite - (hyp _ _ ty zy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)