proposition: Theorem inbetween_plus_compat : forall x d u l t, inbetween x d u l -> inbetween (x + t) (d + t) (u + t) l.
proof: Proof. intros x d u l t [Hx|l' Hx Hl] ; constructor. now rewrite Hx. now split ; apply Rplus_lt_compat_r. replace ((x + t + (d + t)) / 2)%R with ((x + d) / 2 + t)%R by field. now rewrite Rcompare_plus_r. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop