proposition: Lemma AF_asymmetric x: asymmetric_set x.
proof: Proof. move => u v _ _ uv vu. case: (AF (doubleton u v)); first by apply /nonemptyP; exists u; fprops. move => [y /set2_P]; case => ->; apply/nonemptyP. exists v;fprops. exists u;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)