proposition: Lemma plgs_existence : forall A B, A <> B -> exists C, exists D, Parallelogram_strict A B C D.
proof: Proof. intros. assert(HH:=not_col_exists A B H). ex_and HH C. assert(HH:=plg_existence A B C H). ex_and HH D. exists C. exists D. induction H1. assumption. unfold Parallelogram_flat in H1. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel