proposition: Lemma cong3_cop2__col : forall A B C P Q, Coplanar A B C P -> Coplanar A B C Q -> P <> Q -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q -> Col A B C.
proof: Proof. intros A B C P Q HP HQ HPQ HA HB HC. destruct (col_dec A B C); [assumption|]. destruct (midpoint_existence P Q) as [M HMid]. assert (Per A M P) by (exists Q; Cong). assert (Per B M P) by (exists Q; Cong). assert (Per C M P) by (exists Q; Cong). elim (eq_dec_points A M); intro HAM. treat_equalities. assert_diffs; apply col_permutation_2, cop_per2__col with P; Cop. assert (Col A B M). apply cop_per2__col with P; try apply HUD; assert_diffs; auto. apply coplanar_perm_12, col_cop__cop with Q; Col. apply coplanar_trans_1 with C; Cop; Col. assert (Col A C M). apply cop_per2__col with P; try apply HUD; assert_diffs; auto. apply coplanar_perm_12, col_cop__cop with Q; Col. apply coplanar_trans_1 with B; Cop; Col. apply col_transitivity_1 with M; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar