proposition: Lemma catalan_rec2 n: catalan n.+1 = \sum_(i<n.+1) catalan i * catalan (n-i).
proof: Proof. transitivity (\sum_(i in 'I_n.+1) catalan i * catalan (n-i)) => //. rewrite - cardinal_Dyck_path. set I := (n.*2.+2).-tuple bool. pose h (s: I) := (@inord n (DP_splitb_size s)). set f := (fun t:I => Dyck_path t). rewrite - sum1dep_card (partition_big_imset h f) /=. have ->: [set h x | x in f] = [set: 'I_n.+1 ]. apply/setP => i; rewrite inE;apply/imsetP. have lin: i <= n by rewrite - ltnS //. move: (Dyck_path_exists2 (n-i) i) => /=; set l := _ ++ _. rewrite (subnK lin); move/and3P=> [ha hb hc]. set x := Tuple ha; exists x; first by rewrite /f unfold_in. by rewrite /h /x /= (eqP hc) inord_val. apply: eq_big => // i /=; rewrite !inE // => _. have lin: i <= n by rewrite - ltnS //. transitivity (#|[set s:I | f s && (h s == i) ]|). by rewrite sum1dep_card; apply:eq_card => s; rewrite !inE. rewrite - cardinal_Dyck_path. rewrite - cardinal_Dyck_path. rewrite - cardsX. set I1 := i.*2.-tuple bool. set I2 := ((n-i).*2).-tuple bool. symmetry. set B1 := [set s:I1 | Dyck_path s]. set B2 := [set s:I2 | Dyck_path s]. pose g1 (p: I1 * I2) := p.2 ++ DP_raise (p.1). have gs p: size (g1 p) == n.+1.*2. by rewrite /g1/= size_cat size_DP_raise !size_tuple !addnS - doubleD subnK. pose g p := Tuple (gs p). have injg: injective g. move => s1 s2 /(f_equal (@tval (n.*2.+2) bool)); rewrite /= /g1 => /eqP. rewrite (eqseq_cat) ?size_tuple // => /andP [sa]; rewrite DP_raise_inj => sb. rewrite (surjective_pairing s1) (surjective_pairing s2). move /eqP:sa => /val_inj ->; move /eqP:sb => /val_inj -> //. rewrite card_set_pred -(card_imset _ injg) ;apply: eq_card => x. rewrite !inE; apply/imsetP/idP => [ [y yp yv] | cx]. rewrite yv /f/g /=. move: yp; rewrite !inE => /andP[ dp1 dp2]. move:(DP_splitb_prop4 dp2 dp1) => /and3P [ha hb hc]; rewrite ha /h /=. by rewrite/DP_splitb_size (eqP hc) DP_raiseK size_tuple// doubleK inord_val. move/andP:cx; rewrite /f/h ; move => [sa sb]. have sx: size x = n.+1.*2 by rewrite size_tuple. move:(DP_splitb_size_correct sa sx); rewrite -ltnS; move/andP=> [/eqP sc sd]. have se: DP_splitb_size x = i by rewrite - (eqP sb) (inordK sd). have nn:~~ nilp x by rewrite /nilp size_tuple. move:(DP_splitb_prop3 sa nn) => /andP[ra rb]. move: (DP_splitb_recover x); rewrite (eqP ra) => eqa. move: (f_equal size (DP_splitb_recover x)); rewrite size_cat sx sc se => /eqP. rewrite 2!addnS {2} (doubleS n) 2!eqSS -{3} (subnK lin) doubleD eqn_add2r => su. have sv: size (DP_lower ((DP_splitb x).2)) == i.*2. by move: sc; rewrite se/DP_lower 2! size_behead size_belast => ->. exists (Tuple sv,Tuple su); last by apply:val_inj;rewrite /= - {1} eqa. by rewrite !inE /= rb; move/andP:(DP_splitb_Dyck12 sa) =>[-> //]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)