proposition: Lemma not_ord_example (r:= fun A X Y => [/\ sub X Y, sub X A & sub Y A]): (forall A, order_r (r A)) /\ (forall Y, ~ order_r(fun A X => r A X Y)).
proof: Proof. split. move => A; split. - move => y x z [ha hb hc][hd he hf]; split => //; apply: (sub_trans ha hd). - by move => x y [ha hb hc][hd he hf]; apply: extensionality. - move => x y [ha hb hc]; split; split => //. move => Y [ha hb hc]. have r1 Z: r Z Z Y -> Z = Y by move => [qa qc]; apply: extensionality. have r2: r (Y +s1 Y) emptyset Y by split; fprops. move: (hc _ _ r2) => [/r1 hh /r1 hhh]; empty_tac1 Y; rewrite -{2} hh; fprops. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)