proposition: Lemma comp_eql A B (R : A -> B -> Type) : (eq \o R <= 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)