proposition: Lemma Exercise1_21l r x y: total_order r -> (related (scattered_equiv r) x y <-> (scattered_aux r x y \/ scattered_aux r y x)).
proof: Proof. move=> tor; split. by move /graph_on_P1 => [xsr ysr scxy];case: scxy; move=> [rxy]; move /(Exercise1_21kP tor rxy) => aux;[ left | right]. by case; move=> [xsr aux]; apply /graph_on_P1;split => //; try order_tac; [left | right];split => //; apply / Exercise1_21kP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)