proposition: Lemma Exercise1_21kP r x y: total_order r -> gle r x y -> (scattered (induced_order r (interval_cc r x y)) <-> scattered_aux1 r x y).
proof: Proof. move=> tor xy. have or: order r by move: tor => [or _ ]. set (i:=interval_cc r x y). have si: (sub i (substrate r)) by apply: Zo_S. have usr: (forall u, sub u i -> sub u (substrate r)). move => u ui; apply: (sub_trans ui si). split. move /(Exercise1_21aP or si) => h u ui. apply /(Exercise1_21dP tor (usr _ ui)); apply: (h _ ui). move => hyp; apply /(Exercise1_21aP or si) => u ui. apply /(Exercise1_21dP tor (usr _ ui)) => //; exact (hyp _ ui). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)