proposition: Lemma cut_root : forall (x y : R) (G P : Prop), ((P -> G) -> x = y -> G) -> ((x = y -> P) -> G) -> G.
proof: Proof. intros x y G P K L. destruct (Req_dec x y) as [H|H]. apply K with (2 := H). intros N. now apply L. apply L. intros N. now elim H. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify Interval_helper