proposition: Lemma Exercise1_5e r X: total_order r -> inc X (free_subsets r) -> small_set X.
proof: Proof. move=> [_ t] /Zo_P [] /setP_P xs fs x y xX yX. by case: (t _ _ (xs _ xX) (xs _ yX)) => aux; [ | symmetry ]; apply: fs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)