proposition: Lemma comp_hrelP A B C (R : A -> B -> Type) (R' : B -> C -> Type) (b : B) (a : A) (c : C) : R a b -> R' b c -> (R \o R')%rel a c.
proof: Proof. by exists b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop)