proposition: Lemma substrate_quotient_order r s: preorder_quo_axioms r s -> substrate (quotient_order r s) = quotient s.
proof: Proof. move=> ax;move: (quotient_is_preorder ax)=> pq. set_extens x. by move /(preorder_reflexivity _ pq) /quotient_orderP => [xs _]. move=> xs; apply /(preorder_reflexivity _ pq) /quotient_orderP. have [po es ssr] := ax. split => //y yx; ex_tac; apply /(preorder_reflexivity _ po). rewrite - ssr; apply: (inc_in_setQ_sr es yx xs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)