proposition: Lemma Exercise1_21o r: total_order r -> Ex1_2_hC' r (scattered_equiv r).
proof: Proof. move=> tor; move=> x y z xy yz; move/(Exercise1_21l _ _ tor). move:(Exercise1_21i tor)(Exercise1_21j tor) => es ss. move: tor => [or tor]; case;move=> [xx hyp]. apply/Exercise1_21l => //;left; split => //. move=> u ui; apply: hyp => //; move=> t tu; move: (ui _ tu) => /Zo_P. move=> [tsr [xt ty]]; apply /Zo_P; split => //;split => //; order_tac. have leyx: (gle r y x) by order_tac. have <-: (x = y) by order_tac. have:(inc x (substrate r)) by order_tac. rewrite - ss=> xsr;equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)