proposition: Lemma zequiv_sub a b a': ziequivalent a b -> sub a' a -> exists b', (sub b' b /\ ziequivalent a' b').
proof: Proof. move=> [pa [f zm]] a'a. move: (zmap_sub zm a'a) => [f' [b' [pb pc pd]]]; exists b';split => //. split; [ apply: (sub_disjoint pa a'a pc) | by exists f']. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)