proposition: Lemma compg_pP r r' x y: inc (J x y) (r' \cg r) <-> (exists2 z, inc (J x z) r & inc (J z y) r').
proof: Proof. apply: (iff_trans (compg_P _ _ _) ); aw. split;[ by case | move => h; fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)