proposition: Lemma compg_S r r' s s': sub r s -> sub r' s' -> sub (r' \cg r) (s' \cg s).
proof: Proof. move=> rs rs' t /compg_P [ {3} <- [ x ir ir']]. by apply/compg_pP; exists x; [apply: rs | apply: rs']. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)