proposition: Lemma comp_eqr A B (R : A -> B -> Type) : (R \o eq <= R)%rel.
proof: Proof. by move=> x y [y' [? <-]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop)