fact: Definition hrespectful (A B C D : Type) (R : A -> B -> Type) (R' : C -> D -> Type) : (A -> C) -> (B -> D) -> Type := fun f g => forall (x : A) (y : B), R x y -> R' (f x) (g y).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop)