proposition: Lemma eq_hrelLR A B (R R' : A -> B -> Type) : (R <=> R')%rel -> (R' <= R)%rel.
proof: Proof. by case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop)