proposition: Lemma grec1_propagate A (Fi : A -> nat -> A) (Gi : A -> nat -> I.type) ai si : (forall qi m, I.convert (Gi qi m) = Inan) -> seq_eqNai si -> forall n, poly_eqNai (grec1 Fi Gi ai si n).
proof: Proof. move=> HG Hs n k Hk. rewrite /grec1 /size size_grec1up ltnS in Hk. rewrite /grec1 /nth nth_grec1up. rewrite ltnNge Hk /=. case: ltnP => H2. - exact: Hs. - exact: HG. 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