proposition: Lemma ci_image A B: sub A B -> Imf (canonical_injection A B) = A.
proof: Proof. move => h; move:(ci_fp h) => [ff sf tf]. set_extens t. by move/(Imf_P ff); rewrite sf;move => [u uA ->]; rewrite ci_V. by move => tA; apply/(Imf_P ff); rewrite sf; ex_tac;rewrite ci_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)