proposition: Lemma catalan_spec m k (n := (m + k.+1).*2.+1): ( 'C(n, m) < 'C(n, m.+2)) && ( (m+ k.*2.+3) * ('C(n, m.+2)-'C(n, m)) == 'C(n.+1, m.+2)* k.*2.+1 ).
proof: Proof. have hx: m.+2 <= n. by rewrite ltnS -addSnnS -addnn -addnA leq_addr. have hz:= (leq_trans hx (leqnSn _)). set z := 'C(n.+1, m.+2). suff h: ((m + k.*2.+3) * ('C(n, m.+2) - 'C(n, m)) == z * k.*2.+1). have: 0 < z * k.*2.+1 by rewrite muln_gt0 bin_gt0 hz //. by rewrite h andbT -{1} (eqP h) muln_gt0 addnS subn_gt0. have czp: 0 < (m.+2)`! * (n.+1 - m.+2)`! by rewrite muln_gt0 !fact_gt0. have cxp: 0< ((m.+2)`! * (n - m.+2)`!) by rewrite muln_gt0 !fact_gt0. set s := (m + k.*2.+2) * (m + k.*2.+3). have cyp: 0 < s by rewrite muln_gt0 addnS /= addnS /=. have eq4: (m + k.*2.+1)`! * s = (m + k.*2.+3)`!. by rewrite /s mulnA !addnS -2!factSr. have eq1: (n.+1 - m.+2)`! = (m + (k.+1).*2)`!. by rewrite /n addnC -addnn addnACA addnn addnA -2!addnS addnK addnC. have eq2: (n - m.+2)`! = (m + (k.*2.+1))`!. by rewrite /n -addSnnS -addnn addnACA (addnn k) addnAC addSnnS -addnS addnK. have eq3: n - m = m + k.*2.+3. by rewrite /n - addnn addnACA - addnA addnn -2!addnS addKn. rewrite - (eqn_pmul2r czp) (mulnAC z) (bin_fact hz) eq1. rewrite (mulnC _ (_ -_ )) - mulnA (mulnCA _ (m.+2)`!) addnS -factS -addnS. set t := ((m.+2)`! * ((m + k.*2.+3))`!). rewrite - (eqn_pmul2r cxp) mulnAC mulnBl (bin_fact hx) eq2. rewrite -(eqn_pmul2r cyp) mulnAC mulnBl -(mulnA 'C(n, m)) -(mulnA (m.+2)`!) eq4. rewrite {1} factS factS (mulnA m.+2) - (mulnA (m.+2 * m.+1)) mulnCA -{1}eq3. rewrite (bin_fact (ltnW (ltnW hx))) (mulnC _ n`!) - mulnBr -/t -4!mulnA. rewrite (mulnC _ s) {2} /s (mulnC (m + k.*2.+2)) -(mulnA _((m + k.*2.+2))). rewrite addnS (addnS _ k.*2.+1) - 2!factS - 2!addnS -/t factSr. rewrite - mulnA (mulnA n.+1); apply/eqP; congr (n`! * (_ * t)). rewrite /s -4!addSnnS mulnDr mulnDl - addnA mulnSr - addnA addKn addnA. by rewrite - mulSn mulnC - mulnDl addnA addnn - doubleD addSnnS addSn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)