proposition: Lemma behead_rec2down n : behead (rec2down n.+1) = rec2down n.
proof: Proof. by case: n => [//|n]; rewrite behead_loop2. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp