proposition: Lemma behead_rec1down n : behead (rec1down n.+1) = rec1down n.
proof: Proof. by rewrite /rec1down; case: (loop1S_ex n 1 a0 [:: a0])=> [c ->]. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp