proposition: Lemma head_rec2downSS n : head d (rec2down n.+2) = F (hb d (rec2down n.+1)) (head d (rec2down n.+1)) n.+2.
proof: Proof. by case: n => [//|n]; rewrite head_loop2S ?addn2. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp