proposition: Lemma split_couple_eq : forall {a b c d : R}, (a,b) = (c,d) -> a = c /\ b = d.
proof: Proof. intros. injection H. intros. split. - subst. reflexivity. - subst. reflexivity. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon