proposition: Lemma eqv_smallest_prop E R (r := (eqv_smallest E R)): (forall x y, R x y -> inc x E /\ inc y E) -> equivalence_on r E /\ eqv_smaller R r.
proof: Proof. move => ha. have hb:equivalence r. apply: setIrel_equivalence. by move => t /Zo_P [/equivalencesP []]. have ne:nonempty (Zo (equivalences E) (eqv_smaller R)). exists (coarse E); apply/Zo_P; split. apply: inc_coarse_all_equivalence_relations. by move => x y /ha /coarse_related. have sr: substrate r = E. by apply:(setIrel_sr ne) => t /Zo_P [/equivalencesP []] // []. split => // x y rxy. by apply/(setI_P ne) => s /Zo_P [uu]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)