proposition: Theorem behead_grec1down (n : nat) : behead (grec1down n.+1) = grec1down n.
proof: Proof. pose s := rev init. pose m := size init. rewrite !grec1downE. case: (leqP (size init) n) => H. rewrite leqW // subSn //. have [c Hc] := gloop1S_ex (n - m).+1 m a0 s. by rewrite Hc. rewrite leq_eqVlt in H; case/orP: H; [move/eqP|] => H. rewrite -H subnn /= ifT H //. by rewrite take_oversize. rewrite ifF 1?leqNgt ?H //. by rewrite behead_rev_take. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp