proposition: Lemma rec1_propagate (Fi : I.type -> nat -> I.type) ai : (forall qi m, I.convert qi = Inan -> I.convert (Fi qi m) = Inan) -> I.convert ai = Inan -> forall n, poly_eqNai (rec1 Fi ai n).
proof: Proof. move=> HF Ha n k Hk. rewrite /size size_rec1up ltnS in Hk. rewrite /nth /rec1. rewrite (nth_rec1up_indep (d2 := I.zero) (m2 := k)) //. rewrite nth_rec1up_last. rewrite last_rec1up head_loop1 //. elim: k Hk => [//|k IHk] Hk /=. apply: HF. apply: IHk. exact: ltnW. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec