proposition: Lemma injective_split : forall n n1 n2 n3 n4 (H1 : n = n1 + n2) (H2 : n3 + n4 = n) f, injective f -> injective (fun k : ordinal n => cast_ord H2 (unsplit (f (split (cast_ord H1 k))))).
proof: Proof. intros n n1 n2 n3 n4 H1 H2 f Hf. apply inj_comp with (f := cast_ord H2). apply cast_ord_inj. apply inj_comp with (f := @unsplit _ _). eapply can_inj. apply unsplitK. apply inj_comp with (1 := Hf). apply inj_comp with (f := @split _ _). eapply can_inj. apply splitK. apply cast_ord_inj. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)