proposition: Lemma equivalence_associated_o_sr r: preorder r -> substrate (equivalence_associated_o r) = substrate r.
proof: Proof. move=> pr. have eq:= (equivalence_preorder1 pr). set_extens x => xs. move: (reflexivity_e eq xs) => /eao_P [pa _]; order_tac. move: pr=> [gr rr _]. by apply: (arg1_sr (y:=x)); move : (rr _ xs) => t;apply/eao_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)