proposition: Lemma Exercise1_21m r: total_order r -> weak_order_compatibility r (scattered_equiv r).
proof: Proof. move=> tor; move: (tor) => [or tor']. move: (Exercise1_21i tor) => es. move: (Exercise1_21j tor) => ss. split => //; first by split => //; by apply: order_preorder. move=> x y x' xy. have ysr: (inc y (substrate r)) by order_tac. move: (ysr); rewrite - ss => yss. have seyy: (related (scattered_equiv r) y y) by equiv_tac. case/ (Exercise1_21l x x' tor) => - [xx' sc]; last first. exists y => //; order_tac. have x'sr: inc x' (substrate r) by order_tac. case: (tor' _ _ ysr x'sr) => yx'; last by exists y. exists x'=> //;last (by order_tac);apply /Exercise1_21l=> //;left; split=> //. move=> u ui; apply: sc; move => t tu; move: (ui _ tu) => /Zo_P [tsr [xt tx']]. apply /Zo_P;split => //; split => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)