proposition: Lemma characterization_of_parallelism_F_aux : forall A B C D, Par A B C D <-> A <> B /\ C <> D /\ exists P, Midpoint C A P /\ exists Q, Midpoint Q B P /\ Col C D Q.
proof: Proof. intros; split; intro H; [do 2 (split; try solve [assert_diffs; auto])| destruct H as [HAB [HCD [P [HP [Q [HQ HCol]]]]]]]. { destruct (symmetric_point_construction A C) as [P HP]; exists P; split; [assumption|]; destruct (midpoint_existence B P) as [Q HQ]. exists Q; split; [assumption|]. assert (Par B A Q C) by (assert_diffs; apply triangle_mid_par with P; Col). destruct (parallel_uniqueness A B C D C Q C); Col; Par. } { assert (Par B A Q C) by (apply triangle_mid_par with P; Col). apply par_col_par with Q; Col; Par. } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems