proposition: Lemma prop_31 : forall A B C, B <> C -> exists E, Par B C A E.
proof: Proof. intros A B C. apply parallel_existence1. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions