proposition: Lemma strict_from_fP (fz : Z) : injective fz.1 -> strictf (strict_from_f fz) /\ same_codom fz.1 (strict_from_f fz).
proof: Proof. move => hf. rewrite /strict_from_f. case: injectiveP => [hinj | []] //; exact: strict_fromP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor