proposition: Lemma rec2up_correct fi f fi0 f0 fi1 f1 n : (forall ai bi a b m, Rel a ai -> Rel b bi -> Rel (f a b m) (fi ai bi m)) -> Rel f0 fi0 -> Rel f1 fi1 -> RelP (rec2up f f0 f1 n) (rec2up fi fi0 fi1 n).
proof: Proof. move=> Hf Hf0 Hf1 k. case: (ltnP n k) => Hn; first by rewrite !nth_default ?size_rec2up. have H1 : k = (size (rec2up f f0 f1 k)).-1 by rewrite size_rec2up. have H2 : k = (size (rec2up fi fi0 fi1 k)).-1 by rewrite size_rec2up. rewrite (@nth_rec2up_indep _ _ _ _ dv dv n k k) // (@nth_rec2up_indep _ _ _ _ dt dt n k k) //. case: k Hn {H1 H2} => [//|k] Hn. rewrite !(nth_rec2up_last, last_rec2up). elim: k {-2}k (leqnn k) Hn => [|k IHk] k' Hk' Hn. - by rewrite leqn0 in Hk'; move/eqP: Hk'->. - rewrite leq_eqVlt in Hk'; case/orP: Hk'=> Hk'; last exact: IHk =>//. move/eqP: (Hk')->; rewrite !head_loop2S //; apply: Hf. + case: k IHk Hn Hk' => [|k] IHk Hn Hk' //. rewrite /hb !behead_loop2. apply: IHk =>//. move/eqP in Hk'; rewrite Hk' in Hn; apply: ltnW; exact: ltnW. + apply: IHk =>//. move/eqP in Hk'; rewrite Hk' in Hn; exact: ltnW. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp