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