proposition: Lemma sub_disjoint a b a' b': disjoint a b -> sub a' a -> sub b' b -> disjoint a' b'.
proof: Proof. move=> di sa sb; apply: disjoint_pr => u ua ub. red in di; empty_tac1 u; saw. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)