proposition: Lemma eqv_smallest_sym E (R: relation): (forall x y, R x y -> inc x E /\ inc y E) -> (eqv_smallest E R) = (eqv_smallest E (fun x y => R x y \/ R y x)).
proof: Proof. move => ha. set R' := (fun x y : Set => R x y \/ R y x). rewrite /eqv_smallest. congr intersection; apply: Zo_exten1 => s /equivalencesP[eq ss]. split => h x y. case; [ by apply:h | move/h ; apply:(proj44 eq)]. by move=> rxy; apply:h; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)