proposition: Lemma cfun_eomerge (c1 : connector m) (c2 : connector m) (t : (m + m).-tuple A) : cfun (ceomerge c1 c2) t = teocat (cfun c1 (tetake t)) (cfun c2 (totake t)).
proof: Proof. apply: eq_from_tnth => i. have iLm : i < m + m by apply: ltn_ord. have i2Lm : i./2 < m by have := ltn_ord (idiv2 i); rewrite val_idiv2. pose a := tnth t i. rewrite /= !(tnth_nth a) /= ?nth_cat !(nth_map i) /=; last 2 first. - by rewrite -fintype.enumT -enum_ord size_enum_ord. - by rewrite -enum_ord size_enum_ord. set u := nth i _ _; have -> : u = i. by apply/val_eqP; rewrite /= /u -fintype.enumT -enum_ord /= nth_enum_ord. rewrite !ffunE {u}nth_eocat; last by rewrite !size_map. have [iO|iE] := boolP (odd i). rewrite !(nth_map (idiv2 i)); last 2 first. - by rewrite -fintype.enumT -enum_ord size_enum_ord. - by rewrite -enum_ord size_enum_ord. set u := nth _ _ _; have -> : u = idiv2 i. apply/val_eqP; rewrite /= /u. by rewrite -fintype.enumT -enum_ord /= !nth_enum_ord ?val_idiv2. rewrite !(tnth_nth a) /= !nth_otake /= val_olift /= val_idiv2. have F : i = i./2.*2.+1 :> nat by rewrite -[LHS]odd_double_half iO. by rewrite -F {1}F ltnS leq_double. rewrite !(nth_map (idiv2 i)); last 2 first. - by rewrite -fintype.enumT -enum_ord size_enum_ord. - by rewrite -enum_ord size_enum_ord. set u := nth _ _ _; have -> : u = idiv2 i. apply/val_eqP; rewrite /= /u. by rewrite -fintype.enumT -enum_ord /= !nth_enum_ord ?val_idiv2. rewrite !(tnth_nth a) /= !nth_etake /= val_elift /= val_idiv2. have F : i = i./2.*2 :> nat by rewrite -[LHS]odd_double_half (negPf iE). by rewrite -F {1}F leq_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple