proposition: Lemma cardinal_fun_image t g : {inc t &, injective g} -> fun_image t g =c t.
proof: Proof. move => H; symmetry; apply /card_eqP. exists (Lf g t (fun_image t g)); saw; apply /lf_bijective. + move=> s sa; apply /funI_P; ex_tac. + exact H. + by move => y /funI_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)