proposition: Lemma substrate_sub: {compat substrate : x y / sub x y}.
proof: Proof. move => r s rs; move: (domain_S rs) (range_S rs) => pa pb t. case /setU2_P => h; apply/setU2_P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)