proposition: Lemma Exercise1_21j r: total_order r -> substrate (scattered_equiv r) = substrate r.
proof: Proof. move=> tor; apply: graph_on_sr. by move=> a asr; move: (Exercise1_21h tor) => [_ rr]; rewrite -rr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)