proposition: Lemma rcons_unique_correct : forall e l, exists l', rcons_unique e l = l ++ l'.
proof: Proof. induction l as [ | e' l [l' IHl]]. - now exists (e :: nil). - simpl. destruct expr_beq. + exists nil. apply app_nil_end. + exists l'. now rewrite IHl. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree