proposition: Lemma rec1_correct fi f fi0 f0 n : (forall ai a m, ai >: a -> fi ai m >: f a m) -> fi0 >: f0 -> rec1 fi fi0 n >:: PolR.rec1 f f0 n.
proof: Proof. move=> Hf Hf0. by apply: (rec1up_correct (Rel := fun r i => i >: r)); first exact: J.zero_correct. 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