proposition: Lemma worderr_total r x y: worder_r r -> r x x -> r y y -> (r x y \/ r y x).
proof: Proof. move => [p1 p2] rxx ryy. move:(set2_1 x y)(set2_2 x y);set (u:=doubleton x y) => xu yu. have p3: {inc u, reflexive_r r} by move => a /set2_P; case => ->. have p4: nonempty u by ex_tac. have p5:(substrate (graph_on r u)) = u by apply: graph_on_sr. move: (p2 _ p3 p4)=> [z []]; rewrite p5 => zu zle. move: (zle _ xu) => /graph_on_P1 [_ _ zx]. move: (zle _ yu) => /graph_on_P1 [_ _ zy]. by case /set2_P: zu => <-; [left | right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)