fact: Definition zbijective F a b := [/\ (forall x, inc x a -> inc (F x) b) , (forall x x', inc x a -> inc x' a -> F x = F x' -> x = x') & (forall y, inc y b -> exists2 x, inc x a & y = F x)].
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)