proposition: Lemma compf_correspondence r' r: correspondence r -> correspondence r' -> correspondence (r' \co r).
proof: Proof. rewrite/compose=> cr cr'; apply: corresp_create. move=>t /compg_P [pt [y ir ir']]; apply:setX_i => //. by move /setX_P: ((proj2 cr) _ ir) => [_ pa _];move: pa; aw. by move /setX_P: ((proj2 cr') _ ir');aw; move => [_ _ pb]; move: pb; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)