proposition: Lemma maximal_inclusion_aux: let s := emptyset in finite_character s /\ ~ (exists x, maximal (sub_order s) x).
proof: Proof. split. move=> x; split; first by move => /in_set0. move=> h; have: (inc emptyset emptyset). apply: h;split; [ fprops | apply: emptyset_finite]. by move /in_set0. by move=> [x [xe _]]; move: xe;rewrite (proj2 (sub_osr _))=> /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)