proposition: Theorem inbetween_mult_reg : forall x d u l s, (0 < s)%R -> inbetween (x * s) (d * s) (u * s) l -> inbetween x d u l.
proof: Proof. intros x d u l s Hs H. generalize (inbetween_mult_compat _ _ _ _ _ (Rinv_0_lt_compat s Hs) H). assert (K: forall y, (y * s * /s = y)%R). { intros y. field. now apply Rgt_not_eq. } now rewrite 3!K. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop