proposition: Lemma DP_lower_DyckK s: Dyck_path s -> ~~ nilp s -> DP_raise (DP_lower s) = s.
proof: Proof. case: s => // a l /and3P [sa sb _] _; rewrite DP_lowerK //. move:sa; case: a; rewrite /DP_balanced /= add0n add1n => /eqP h. by move: (DP_posW sb); rewrite -h ltnn. by case:l sb h => // a l p _; elim: l a p => [ [] | a l H b /andP [/H ]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)