proposition: Lemma sub_hresp_comp A B C (R1 R1' : A -> B -> Prop) (R2 R2' : B -> C -> Prop) : (((R1 ==> R1') \o (R2 ==> R2')) <= ((R1 \o R2) ==> (R1' \o R2')))%rel.
proof: Proof. move=> f h [g [rfg rgh]] x z [y [rxy ryz]]; exists (g y). by split; [apply: rfg | apply: rgh]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset bigop)