proposition: Lemma afa_ex1 x: x <> \Po x.
proof: Proof. set A := Zo x (fun z => ~ inc z z) => h. have aux: ~(inc A A). move /Zo_P => [pa pb]; apply: (pb); apply/Zo_P; split => //. apply: (aux); apply:Zo_i => //; rewrite h; apply /setP_P; apply:Zo_S. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)