proposition: Lemma head_rec1downS n : head d (rec1down n.+1) = F (head d (rec1down n)) n.+1.
proof: Proof. by rewrite head_loop1S ?addn1. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp