proposition: Lemma composableE A B C (rAB : A -> B -> Type) (rBC : B -> C -> Type) (rAC : A -> C -> Type) : composable rAB rBC rAC = (rAB \o rBC <= rAC).
proof: Proof. by rewrite /composable unlock. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching