proposition: Lemma subon_bij (D2' : pred T2) : {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f}.
proof: Proof. by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K]. Qed.
imports: ssreflect ssrfun