proposition: Lemma no_floor_prog_rev prog : no_floor_prog (rev prog) = no_floor_prog prog.
proof: Proof. elim prog; simpl; try easy. intros a l IH. now rewrite no_floor_prog_rcons IH no_floor_prog_cons. 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