proposition: Lemma playfair__existential_playfair : playfair_s_postulate -> existential_playfair_s_postulate.
proof: Proof. intro HF. exists PA, PB, PC. split; [apply lower_dim|]; intros; apply HF with PA PB PC; assumption. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Definitions