proposition: Theorem inbetween_plus_reg : forall x d u l t, inbetween (x + t) (d + t) (u + t) l -> inbetween x d u l.
proof: Proof. intros x d u l t H. generalize (inbetween_plus_compat _ _ _ _ (Ropp t) H). assert (K: forall y, (y + t + -t = y)%R) by (intros y ; ring). now rewrite 3!K. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop