proposition: Lemma Exercise1_2a r s: preorder_quo_axioms r s -> preorder_r (quotient_order_r r s).
proof: Proof. move=> [ [gr rr tr] es sssr]; split. move=> a b c [aq bq abp] [_ cq bcp];split => //. move => x /abp [y /bcp [z zc yz] xy]; ex_tac; apply: tr xy yz. move=> a b [aq bq abp]. by split; split => // x xs; ex_tac; apply: rr; rewrite - sssr; apply: (inc_in_setQ_sr es xs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)