proposition: Lemma rec2_correct fi f fi0 f0 fi1 f1 n : (forall ai bi a b m, ai >: a -> bi >: b -> fi ai bi m >: f a b m) -> fi0 >: f0 -> fi1 >: f1 -> rec2 fi fi0 fi1 n >:: PolR.rec2 f f0 f1 n.
proof: Proof. move=> Hf Hf0 Hf1. by apply: (rec2up_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