proposition: Lemma ci_fp A B: sub A B -> function_prop (canonical_injection A B) A B.
proof: Proof. move => sAB; split; first by apply:ci_f. rewrite /canonical_injection; aw; trivial. by rewrite /canonical_injection; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)