proposition: Lemma ci_compose A B C (fAB := canonical_injection A B) (fBC := canonical_injection B C)(fAC := canonical_injection A C): sub A B -> sub B C -> fBC \co fAB = fAC.
proof: Proof. move => hAB hBC; move: (sub_trans hAB hBC) => hAC. move:(ci_fp hAB)(ci_fp hBC)(ci_fp hAC)=>[fij sij tij][fjk sjk tjk][fik sik tik]. have co: fBC \coP fAB by split => //; ue. apply: function_exten;aw; trivial;try ue; first by apply: compf_f. move => x xs /=; rewrite compfV //. have xA: inc x A by ue. have xB: inc x B by apply: hAB. by rewrite /fAB /fBC /fAB /canonical_injection !ci_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)