proposition: Lemma eqv_smallest_prop2 E (R: relation) r: (forall x y, R x y -> inc x E /\ inc y E) -> equivalence_on r E -> eqv_smaller R r -> (forall r', equivalence_on r' E -> eqv_smaller R r' -> sub r r') -> r = eqv_smallest E R.
proof: Proof. move => ep er sm h. set F := (Zo (equivalences E) (eqv_smaller R)). have ha: inc r F by apply/Zo_P; split => //; apply/equivalencesP. move:(eqv_smallest_prop ep) => [hb hc]; move:(h _ hb hc) => sub1. by apply: extensionality => //; apply:setI_s1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)