proposition: Theorem inbetween_unique : forall l l', inbetween l -> inbetween l' -> l = l'.
proof: Proof. intros l l' Hl Hl'. inversion_clear Hl ; inversion_clear Hl'. apply refl_equal. rewrite H in H0. elim Rlt_irrefl with (1 := proj1 H0). rewrite H1 in H. elim Rlt_irrefl with (1 := proj1 H). apply f_equal. now rewrite <- H0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop