proposition: Lemma no_floor_prog_cons t prog : no_floor_prog (t :: prog) = no_floor_term t && no_floor_prog prog.
proof: Proof. unfold no_floor_prog. generalize true. revert t; elim prog; simpl. now intros t b; case b; case no_floor_term. intros a l IH t b. now rewrite !IH; case no_floor_term; simpl; case no_floor_term; simpl. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog