proposition: Lemma rec1up_correct fi f fi0 f0 n : (forall ai a m, Rel a ai -> Rel (f a m) (fi ai m)) -> Rel f0 fi0 -> RelP (rec1up f f0 n) (rec1up fi fi0 n).
proof: Proof. move=> Hf Hf0 k. case: (ltnP n k) => Hnk; first by rewrite !nth_default ?size_rec1up. have H1 : k = (size (rec1up f f0 k)).-1 by rewrite size_rec1up. have H2 : k = (size (rec1up fi fi0 k)).-1 by rewrite size_rec1up. rewrite (@nth_rec1up_indep _ _ _ dv dv n k k) // (@nth_rec1up_indep _ _ _ dt dt n k k) //. rewrite !(nth_rec1up_last, last_rec1up). rewrite !head_loop1 //. elim: k Hnk {H1 H2} => [|k IHk] Hnk //=. apply: Hf; apply: IHk; exact: ltnW. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp